## Stream: new members

### Topic: Help with Proving a Simple Theorem

#### Dev-Indra (Apr 25 2020 at 01:00):

Here is the lemma I am trying to prove (along with my definitions)

def dvd (m n: ): Prop :=  k, n = m * k
def prime (p : ) : Prop := p  2   n, dvd n p  n = 1  n = p
def composite (d : ): Prop:=  (a b: ), d = a*b  a  b  b < d

lemma dvd_n_less_than_n (u n : ) (ha: dvd u n)(hb: u1 )(hc: u n) : u < n :=
begin
rw dvd at ha,
cases ha with k hk,
rw hk,

end

Here is my tactic state after rw hk

1 goal
u n : ,
hb : u  1,
hc : u  n,
k : ,
hk : n = u * k
u < u * k

I have tried proving this with linarith but that hasn't worked. Can anyone help me prove this lemma?

#### Shing Tak Lam (Apr 25 2020 at 01:33):

You haven't got strong enough assumptions in your lemma statement. You also need that n ≠ 0.

#### Bryan Gin-ge Chen (Apr 25 2020 at 01:33):

Here's the first thing I could get to work with that hypothesis:

import data.nat.basic

def dvd (m n: ): Prop :=  k, n = m * k

lemma dvd_n_less_than_n (u n : ) (ha: dvd u n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
cases ha with k hk,
subst hk,
rw lt_mul_iff_one_lt_right,
{ cases k,
{ cases k,
{ simp at hc, contradiction, },
{ simp [nat.succ_lt_succ], } } },
{ cases u,
{ simp at hc, contradiction, },
{ simp, } }
end

This can probably be simplified greatly.

#### Mario Carneiro (Apr 25 2020 at 01:40):

lemma dvd_n_less_than_n (u n : ) (ha: dvd u n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
refine lt_of_le_of_ne _ hc,
rcases ha with k, rfl,
simpa using nat.mul_le_mul_left _ (_:1≤_),
refine nat.pos_iff_ne_zero.2 (mt _ hn),
rintro rfl, refl,
end

#### Reid Barton (Apr 25 2020 at 01:42):

Ah, this is a custom dvd. Otherwise the last four lines are in the library already.

#### Bryan Gin-ge Chen (Apr 25 2020 at 01:57):

For completeness:

lemma dvd_n_less_than_n' (u n : ) (ha: u  n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
refine lt_of_le_of_ne _ hc,
exact nat.le_of_dvd (nat.pos_of_ne_zero hn) ha,
end

Last updated: May 10 2021 at 18:22 UTC