Theorem: exercise4_4 (LeanCourse/Assignments/Assignment4.lean)

State before:
n : ℕ
⊢ ¬Nat.Prime n ↔ n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
sorry
State after:
no goals