proposition: Lemma Even_or_Odd : forall x, Even x \/ Odd x.
proof: Proof. intro x; nzinduct x. - left. exists 0. now nzsimpl. - intros x. split; intros [(y,H)|(y,H)]. + right. exists y. rewrite H. now nzsimpl. + left. exists (S y). rewrite H. now nzsimpl'. + right. assert (LT : exists z, z<y). * destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x]. rewrite <- le_succ_l, H. nzsimpl'. rewrite <- (add_0_r y) at 3. now apply add_le_mono_l. * destruct LT as (z,LT). destruct (lt_exists_pred z y LT) as (y' & Hy' & _). exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'. + left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. Qed.
imports: Bool NZAxioms NZMulOrder