proposition: Lemma plus_cons_cons_rw2 : forall a n b n' b', nf (cons a n b) -> nf (cons a n' b') -> plus (cons a n b) (cons a n' b')= cons a (S (n + n') ) b'.
proof: Proof. simpl. destruct a. intros. rewrite (nf_of_finite H0). auto. rewrite (compare_rw2). auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List