Coq Proof Assistant

Interactive theorem proving: goals, hypotheses, and tactics

n + 0 = n A ∧ B → B ∧ A A ∨ B → B ∨ A ¬¬A → A (classical) length (rev l) = length l

Theorem Statement

Apply Tactic

Click tactics to advance the proof

Proof State

Select a theorem to begin

Proof Script