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