proposition: Lemma rec2_princ : forall P : Z -> Prop, P 0%Z -> (forall x : Z, Zeven.Zeven x -> (x > 0)%Z -> P (Zeven.Zdiv2 x) -> P x) -> (forall x : Z, Zeven.Zodd x -> (x > 0)%Z -> P (x - 1)%Z -> P x) -> forall x : Z, (x >= 0)%Z -> P x.
proof: Proof. intros; apply natgen_ind; intros. case (Z_le_lt_eq_dec 0 x0 H3); intro. case (Zeven.Zeven_odd_dec x0); intro. apply H0. auto. omega. apply H4. apply Zge_le; apply Zdiv2_positive; [ trivial | omega ]. apply Zgt_lt; apply x_gt_Zdiv2; [ trivial | omega ]. apply H1. trivial. omega. apply H4; omega. rewrite <- e; trivial. omega. Qed.
imports: ZArith Omega