proposition: Lemma odd_spec : forall n, odd n = true <-> Odd n.
proof: Proof. unfold odd. fix odd_spec 1. intro n; destruct n as [|[|n]]; simpl. - split; [ discriminate | intro H; elim (Odd_0 H) ]. - split; [ intros; apply Odd_1 | trivial ]. - rewrite odd_spec. apply Odd_2. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass