proposition: Lemma plus_compat: forall n p, F n + F p = F (n + p)%nat.
proof: Proof. induction n; destruct p; simpl ; auto. rewrite <- (plus_n_O n);auto. rewrite plus_n_Sm;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List