proposition: Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.
proof: Proof. intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x). replace (x + 0) with x; auto with arith. Defined.
imports: Arith