proposition: Lemma omega_term_plus_rw: 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. + reflexivity. + intro H. now apply nf_inv3, compare_gt_iff in H as ->. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)