km < kn => m < n

Stream: new members

[Li Xuanji]

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]

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

[Li Xuanji]

ah thanks!

[Li Xuanji]

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]

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

[Kevin Buzzard]

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]

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

[Li Xuanji]

@Kevin Buzzard thanks!

[Li Xuanji]

@Reid Barton I think that implies my statement

[Li Xuanji]

actually I'm not sure

[Reid Barton]

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]

oops, I named both statements lt_mul_cancel

[Li Xuanji]

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

[Reid Barton]

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]

oh yeah I see what you mean