proposition: Lemma T1lt_iff a b: T1nf a -> T1nf b -> a < b <-> g2h a t1< g2h b.
proof: Proof. move => Ha Hb; split. - rewrite -(h2g_g2hK a) -(h2g_g2hK b); repeat split. 1, 3: by rewrite g2h_h2gK hnf_g2h. + by rewrite !h2g_g2hK hlt_iff. - destruct 1 as [H0 [H1 H2]]. by rewrite -(h2g_g2hK a) -(h2g_g2hK b) -hlt_iff. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)