proposition: Lemma plus_cons_cons_rw3 : forall a n b a' n' b', a' < a -> nf (cons a n b) -> nf (cons a' n' b') -> cons a n b + cons a' n' b'= cons a n (b + (cons a' n' b')).
proof: Proof. simpl. destruct a. inversion 1. destruct a'. rewrite compare_rw3. auto. constructor. intros; rewrite compare_rw3. auto. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List