proposition: Lemma LT_inv : forall a n b a' n' b', cons a n b t1< cons a' n' b' -> a t1< a' \/ a = a' /\ (n < n' \/ n = n' /\ b t1< b').
proof: Proof. intros a n b a' n' b' H; case H. - clear H; intros H (H0,H1); case (lt_inv H0). + left; split. * eapply nf_inv1;eauto. * split;auto;eapply nf_inv1;eauto. + intros [(e,i)|(e,(e',i))]. * auto. * right; split; auto. right; split; auto. split. -- eapply nf_inv2; eauto. -- split; [auto | eapply nf_inv2; eauto]. 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)