## Stream: new members

### Topic: km < kn => m < n

#### Li Xuanji (Jun 03 2020 at 15:37):

Does mathlib have this lemma allowing dividing through an inequality?

lemma lt_mul_cancel (n m k : ℕ) (h_k : k > 0) : (k*m < k*n) → (m < n) :=
sorry


I briefly looked through data/nat/lemmas.lean and couldn't find it

#### Shing Tak Lam (Jun 03 2020 at 15:45):

mul_lt_mul_left

library_search finds it btw

import data.nat.basic

lemma lt_mul_cancel (n m k : ℕ) (h_k : k > 0) : (k*m < k*n) → (m < n) :=
(mul_lt_mul_left h_k).1


ah thanks!

#### Li Xuanji (Jun 03 2020 at 16:15):

any hope that this one is in mathlib? library_search didn't find it

lemma lt_mul_cancel (n m k : ℕ) (h_k : k > 1) : (k*m + 1 < k*n) → (m < n) :=
begin
sorry
end


#### Li Xuanji (Jun 03 2020 at 16:16):

if not, would I have to work over \R to prove it?

#### Kevin Buzzard (Jun 03 2020 at 16:35):

lemma lt_mul_cancel (n m k : ℕ) (h_k : 1 < k) : (k*m + 1 < k*n) → (m < n) :=
begin
intro h,
refine lt_of_mul_lt_mul_left _ (show 0 ≤ k, by linarith),
refine lt_trans _ h,
omega,
end


There's a proof which works over nat

#### Reid Barton (Jun 03 2020 at 16:44):

Is this the statement you want? if $km + 1 < kn$ then $km < km + 1 < kn$

#### Li Xuanji (Jun 03 2020 at 16:53):

@Kevin Buzzard thanks!

#### Li Xuanji (Jun 03 2020 at 16:53):

@Reid Barton I think that implies my statement

#### Li Xuanji (Jun 03 2020 at 16:53):

actually I'm not sure

#### Reid Barton (Jun 03 2020 at 16:54):

I thought maybe you got the statement wrong, because it has a stronger hypothesis than lt_mul_cancel so it immediately reduces to that one.

#### Li Xuanji (Jun 03 2020 at 16:59):

oops, I named both statements lt_mul_cancel

#### Li Xuanji (Jun 03 2020 at 17:00):

but I thought they are different, since the second one relies on the fact that 1/k < 1 for most naturalsk

#### Reid Barton (Jun 03 2020 at 17:13):

But k > 1 isn't actually needed for the second one. So either at least one of us is confused, or the statement is the wrong one.

#### Li Xuanji (Jun 04 2020 at 01:34):

oh yeah I see what you mean

Last updated: May 10 2021 at 00:31 UTC