proposition: Lemma plus_to_cons: forall a n b, nf (cons a n b) -> omega_term a n + b = cons a n b.
proof: Proof. simpl. destruct a. intros n b H. rewrite (nf_of_finite H); auto. destruct b. auto. inversion_clear 1. case (trichotomy_inf (cons a1 n a2) b1). destruct 1. absurd (lt b1 b1);eauto with T1. eapply lt_trans;eauto. subst b1. case (lt_irr H0). intro; rewrite compare_rw3; auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List