Zulip Chat Archive

Stream: general

Topic: le for div?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 04 2018 at 17:08):

Don't use le_div_of_mul_le; use le_div_iff_mul_le instead

view this post on Zulip Chris Hughes (Apr 04 2018 at 17:09):

Sorry, I was talking about a div_le not le_div

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Matt Wilson (Apr 04 2018 at 17:19):

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

view this post on Zulip Simon Hudon (Apr 04 2018 at 17:21):

About 51ms on my system

view this post on Zulip Simon Hudon (Apr 04 2018 at 17:22):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:39):

but I haven't seen the div version before

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (Apr 05 2018 at 01:23):

@Mario Carneiro @Simon Hudon How about this? https://github.com/MonoidMusician/mathlib/pull/1 ;)

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (Apr 05 2018 at 01:35):

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

view this post on Zulip 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