## 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: u≠1 )(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