proposition: Lemma Nat_Induction : forall x : Nat, Acc Le x -> forall P : Nat -> Prop, P Z -> (forall x : Nat, P x -> P (SUCC x)) -> P x.
proof: Proof. intros x H. elim H. intros x0. case x0. intros. assumption. intros. apply H3. apply (H1 n). apply Le_n. assumption. assumption. Qed.
imports: Acc_and_Inf