## Stream: general

### Topic: le for div?

#### Nicholas Scheel (Apr 04 2018 at 16:40):

This seems like a silly question but I've scoured mathlib and init for this lemma and I can't find it: ∀ {n m : ℕ} (h : n ≤ m) {k}, n/k ≤ m/k
I don't think it can be derived from div_le_of_le_mul since k*(n/k) = n does not necessarily hold (only if k | n)
a version for multiplication would be nice too
does this exist? is there a nice way to prove it?

#### Simon Hudon (Apr 04 2018 at 16:46):

I think le_div_iff_mul_lewith div_mul_le_self should allow you to prove that

#### Chris Hughes (Apr 04 2018 at 17:07):

It doesn't. Applying le_div_of_mul_le gives you something false to prove, if say n=4, m=5, k=3

#### Simon Hudon (Apr 04 2018 at 17:08):

Don't use le_div_of_mul_le; use le_div_iff_mul_le instead

#### Chris Hughes (Apr 04 2018 at 17:09):

Sorry, I was talking about a div_le not le_div

#### Nicholas Scheel (Apr 04 2018 at 17:11):

Thanks for the tip! :bow: I think I got it working now:

lemma nat.le_mul {n m : ℕ} (h : n ≤ m) {k} : n*k ≤ m*k
:= begin
cases k with k, rw [nat.mul_zero, nat.mul_zero],
apply (nat.le_div_iff_mul_le n (m*nat.succ k) (nat.zero_lt_succ k)).1,
rw [nat.mul_div_left],
exact h,
apply nat.zero_lt_succ,
end

lemma nat.le_div {n m : ℕ} (h : n ≤ m) {k} : n/k ≤ m/k
:= begin
cases k with k, rw [nat.div_zero, nat.div_zero],
apply (nat.le_div_iff_mul_le (n/nat.succ k) (m) (nat.zero_lt_succ k)).2,
transitivity,
apply nat.div_mul_le_self,
exact h,
end


#### Simon Hudon (Apr 04 2018 at 17:18):

A a matter of style, you may prefer cases lt_or_eq_of_le (zero_le k) with hk hk instead of cases k with k

#### Matt Wilson (Apr 04 2018 at 17:19):

peanut gallery question, but how long does that take to run

#### Simon Hudon (Apr 04 2018 at 17:22):

Sorry, wrong proof. @Nicholas Scheel 's proof takes 6ms

#### Simon Hudon (Apr 04 2018 at 19:22):

@Nicholas Scheel Feel free to send a pull request of that theorem to mathlib. You should call it nat.div_le_div.

#### Kevin Buzzard (Apr 04 2018 at 22:39):

 nat.mul_le_mul_right : ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k  is already there

#### Kevin Buzzard (Apr 04 2018 at 22:39):

but I haven't seen the div version before

#### Mario Carneiro (Apr 05 2018 at 01:20):

I'm also surprised to find this is missing. I will add it to mathlib, by the name nat.div_le_div_right

#### Mario Carneiro (Apr 05 2018 at 01:25):

I'm also going to rewrite the proof, since it's a one-liner. I think Simon gave a hint earlier about this, see if you can shorten your proof

#### Nicholas Scheel (Apr 05 2018 at 01:32):

hmm okay, I don’t know enough to see how to shorten it like that and I’ve run out of time tonight, feel free to pick it up if you want :simple_smile:

#### Mario Carneiro (Apr 05 2018 at 01:34):

oh, actually I forgot about the zero case. Anyway here's my attempt at shortening it:

protected theorem div_le_div {n m : ℕ} (h : n ≤ m) {k : ℕ} : n / k ≤ m / k :=
(nat.eq_zero_or_pos k).elim (λ k0, by simp [k0]) $λ hk, (nat.le_div_iff_mul_le _ _ hk).2$ le_trans (nat.div_mul_le_self _ _) h


#### Nicholas Scheel (Apr 05 2018 at 01:35):

(whoops didn’t realize that I PRed my own repo)

#### Mario Carneiro (Apr 05 2018 at 01:37):

looking at the differences, I guess I didn't do much besides compactify the same steps, more or less

Last updated: May 13 2021 at 05:21 UTC