proposition: Lemma odd_OddT : forall n, odd n = true -> OddT n.
proof: Proof. unfold odd. fix odd_specT 1. intro n; destruct n as [|[|n]]; simpl. - intro H; discriminate. - intros; apply OddT_1. - intros He%odd_specT; apply OddT_2; assumption. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass