# Zulip Chat Archive

## 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
```

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

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 naturals`k`

#### 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