proposition: Lemma plus_cons_cons_rw2 : forall a n b n' b', nf (cons a n b) -> nf (cons a n' b') -> cons a n b + cons a n' b' = cons a (S (n + n')) b'.
proof: Proof. cbn; destruct a. - intros n b n' b' H H0; now rewrite (nf_of_finite H0). - now rewrite compare_refl. 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)