proposition: Lemma succ_compat : forall n:nat, succ (F n) = F (S n).
proof: Proof. destruct n; compute ; trivial. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List