proposition: Lemma even_spec : forall n, even n = true <-> Even n.
proof: Proof. fix even_spec 1. intro n; destruct n as [|[|n]]; simpl. - split; [ intros; apply Even_0 | trivial ]. - split; [ discriminate | intro H; elim (Even_1 H) ]. - rewrite even_spec. apply Even_2. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass