proposition: Lemma EvenT_OddT_rect (P Q : nat -> Type) : (forall n, EvenT n -> Q n -> P (S n)) -> Q 0 -> (forall n, OddT n -> P n -> Q (S n)) -> forall n, EvenT n -> Q n.
proof: Proof. intros HQP HQ0 HPQ [|n] HES; [ assumption | ]. assert (OddT n) as HO by apply (EvenT_S_OddT _ HES). apply HPQ, (OddT_EvenT_rect P Q); assumption. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass