## Stream: new members

### Topic: Composite not prime

#### Dev-Indra (Apr 26 2020 at 16:26):

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,
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 (Apr 26 2020 at 16:46):

actually, this was my lemma:

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