proposition: Lemma lt_ref : refinesRel T1.lt T1lt.
proof: Proof. move=> a b; split. - rewrite /Epsilon0.T1.lt /Comparable.compare; move => Hab. generalize (compare_ref a b); now rewrite Hab. - move => Hab; rewrite /T1.lt. case_eq (Epsilon0.T1.compare_T1 a b) => [Heq |//| Hgt]. + generalize (compare_ref a b); rewrite Heq. move => H0; move: Hab; rewrite H0; by rewrite T1ltnn. + generalize (compare_ref a b); rewrite Hgt. move => H1; have H2: (h2g a < h2g a). * eapply T1lt_trans; eauto. * move :H2; by rewrite T1ltnn. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)