proposition: Lemma le_ref : refinesRel T1.le T1le.
proof: Proof. move=> a b; split. - rewrite /T1le /Comparable.compare => Hab; elim: Hab. + move => y Hy; have H: (h2g a < h2g y) by apply lt_ref. * by rewrite H orbT. * by rewrite eq_refl. - rewrite T1le_eqVlt; move => /orP; destruct 1; last first. + left; by rewrite lt_ref. + move: H => /eqP; by rewrite h2g_eqE => ->; right. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)