proposition: Lemma gE0le_iff a beta : E0le a beta <-> E0_g2h a o<= E0_g2h beta.
proof: Proof. split. - rewrite /E0le; destruct a, beta. rewrite /hE0le /T1.LE => /=; repeat split. rewrite T1le_eqVlt => Hle. have Hor : (cnf0 =cnf1 \/ cnf0 < cnf1). { apply Bool.orb_prop in Hle; destruct Hle as [? | ?]. left; apply /eqP => //. right => //. } destruct Hor as [? | Hneq]. * subst; replace i0 with i. -- right. -- apply eq_proofs_unicity_on; decide equality. * left; apply gE0lt_iff; rewrite /E0lt => //. - rewrite /E0le; destruct a, beta; cbn => Hle. destruct (le_lt_eq_dec Hle) as [l | e]. + move: l; rewrite /hE0lt ; cbn; rewrite -T1lt_iff. * by apply T1ltW. * by apply /eqP. * by apply /eqP. + injection e; rewrite g2h_eqE => Heq; subst; apply T1lenn. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)