Composite and DeMorgan

Stream: new members

[Debendro Mookerjee]

Here are two definitions and a theorem:

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:= ¬ prime d

theorem composite_fact (c: ℕ) : composite c ↔ ∃ (a b: ℕ), c = a*b ∧ a ≤ b ∧ b < c:=
begin
    split,
    rw composite,
    rw prime,
end

this is the tactic state:

2 goals
c : ℕ
⊢ ¬(c ≥ 2 ∧ ∀ (n : ℕ), dvd n c → n = 1 ∨ n = c) → (∃ (a b : ℕ), c = a * b ∧ a ≤ b ∧ b < c)

c : ℕ
⊢ (∃ (a b : ℕ), c = a * b ∧ a ≤ b ∧ b < c) → composite c

In the first goal, how do I use DeMorgan's law to foil out the not in the first goals?

[Anne Baanen]

I think the law you're looking for is not_and. A trick for finding rewriting suggestions: the tactic squeeze_simp reports the lemmas that simp can apply