proposition: Lemma succ_is_plus_one: forall a, nf a -> succ a = a + F 1.
proof: Proof. unfold finite. intro c; elim c. compute; trivial. intro c0;case c0. simpl. intros H n c1 H0 H1. rewrite <- plus_n_O; trivial. intros c1 n c2 H n0 c3 H0 H1. simpl. rewrite H0; [trivial | nf_inv]. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List