proposition: Lemma T1le_iff (a b: T1): a <= b <-> T1.le (g2h a) (g2h b).
proof: Proof. split. - rewrite T1le_eqVlt => /orP; case. move => /eqP Heq; subst; right. move => Hlt; left; by rewrite hlt_iff !h2g_g2hK. - rewrite le_ref; by rewrite !h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)