proposition: Lemma OddT_EvenT_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, OddT n -> P n.
proof: Proof. intros HQP HQ0 HPQ. fix OddT_EvenT_rect 1. intros [|[|n]]. - intros [[|k] H0]; inversion H0. - intros _; apply (HQP _ EvenT_0 HQ0). - intros HOSS. assert (EvenT (S n)) as HES by apply (OddT_S_EvenT _ HOSS). assert (OddT n) as HO by apply (EvenT_S_OddT _ HES). apply (HQP _ HES (HPQ _ HO (OddT_EvenT_rect _ HO))). Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass