proposition: Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
proof: Proof. intros x n; generalize x; clear x; induction n as [|n IH]; simpl. - apply P_implies_acc. - intros x H. constructor. intros y [fxy _]. apply IH. rewrite fxy. replace (n + S x) with (S (n + x)); auto with arith. Defined.
imports: Arith