Help with Proving a Simple Theorem

Stream: new members

[Dev-Indra]

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]

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

[Bryan Gin-ge Chen]

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,
    { contradiction, },
    { 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.

[Shing Tak Lam]

(Wrong thread sorry)

[Mario Carneiro]

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]

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

[Bryan Gin-ge Chen]

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