proposition: Lemma compare_rw_lt alpha beta : alpha t2< beta -> compare alpha beta = Lt.
proof: Proof. intros; generalize (compare_reflect alpha beta). case (compare alpha beta); trivial. - intro;subst beta;case (lt_irr H);auto with T2. - intro; case (lt_irr (alpha:=alpha)). eapply lt_trans;eauto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)