proposition: Lemma decide_hltE (a b : hT1): bool_decide (T1.lt a b) = (h2g a < h2g b).
proof: Proof. rewrite /Epsilon0.T1.lt; generalize (compare_ref a b); rewrite /Comparable.compare /=. destruct (decide (Epsilon0.T1.compare_T1 a b = Datatypes.Lt)). - have bd := e ; apply (bool_decide_eq_true _) in bd. by rewrite bd e. - have bd := n; apply (bool_decide_eq_false _) in bd. rewrite bd. destruct (Epsilon0.T1.compare_T1 a b) => //. * by move => ->; rewrite T1ltnn. * move => Hlt; symmetry; apply/negP => Hlt'. have H1 : (h2g b < h2g b) by apply T1lt_trans with (h2g a). move: H1; by rewrite T1ltnn. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)