Composite not prime

Stream: new members

[Dev-Indra]

Here is a converse lemma I'm trying to prove (composite ==> not prime)

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 greater_than_not_zero (n : ℕ)(n ≥ 2): n ≠ 0:=
begin
    exact lattice.ne_bot_of_gt H,
end

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

lemma composite_not_prime (n:ℕ ) (ge: n≥ 2): (¬ (prime n) ↔ composite n) :=
begin
       intros h,
      rw composite at h,
      by_contradiction,
      rw prime at a,

      cases h with a1 ha1,
      cases ha1 with b hb,
end

My tactic state is :

1 goal
n : ℕ,
ge : n ≥ 2,
a : n ≥ 2 ∧ ∀ (n_1 : ℕ), dvd n_1  n → n_1 = 1 ∨ n_1 = n,
a1 b : ℕ,
hb : n = a1 * b ∧ a1 ≤ b ∧ b < n
⊢ false

How do I extract the from for all the variable n_1 and use b as my n_1?

[Dev-Indra]

actually, this was my lemma:

lemma composite_not_prime (n:ℕ ) (ge: n≥ 2): ( composite n ==> ¬ (prime n) ) :=
begin
       intros h,
      rw composite at h,
      by_contradiction,
      rw prime at a,

      cases h with a1 ha1,
      cases ha1 with b hb,
end

[Kevin Buzzard]

[solved in different thread]