proposition: Lemma EvenT_OddT_dec n : EvenT n + OddT n.
proof: Proof. case_eq (even n); intros Hp. - left; apply even_EvenT; assumption. - right; apply odd_OddT. unfold odd; rewrite Hp; reflexivity. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass