proposition: Lemma gE0lt_iff a beta : E0lt a beta <-> E0_g2h a o< E0_g2h beta.
proof: Proof. split. - rewrite /E0lt; destruct a, beta. rewrite /Lt /T1.LT => /=; repeat split. + rewrite /T1.nf nf_ref h2g_g2hK; by apply /eqP. + by rewrite hlt_iff !h2g_g2hK. + rewrite /T1.nf nf_ref h2g_g2hK; by apply /eqP. - rewrite /E0lt; destruct a, beta. rewrite /Lt /T1.LT; destruct 1 as [H [H0 H1]]. move: H0 ; by rewrite hlt_iff !h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)