proposition: Lemma compare_rw_gt alpha beta: beta t2< alpha -> compare alpha beta = Gt.
proof: Proof. intros; generalize (compare_reflect alpha beta). case (compare alpha beta); trivial. - intro H0;subst beta;case (lt_irr H). - 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)