proposition: Lemma even_EvenT : forall n, even n = true -> EvenT n.
proof: Proof. fix even_specT 1. intro n; destruct n as [|[|n]]; simpl. - intros; apply EvenT_0. - intros H; discriminate. - intros He%even_specT; apply EvenT_2; assumption. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass