proposition: Lemma H'_dom alpha beta : E0lt alpha beta -> dominates_strong (H'_ beta) (H'_ alpha).
proof: Proof. move => H; have H' : (hE0lt (E0_g2h alpha) (E0_g2h beta)) by rewrite -gE0lt_iff. case (Epsilon0.Hprime.H'_dom _ _ H') => x Hx; exists x; rewrite /H'_. move => p Hp; apply /ltP; apply Hx; by apply /leP. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)