proposition: Lemma H'_alpha_mono (alpha : E0) : strict_mono (H'_ alpha).
proof: Proof. generalize (Hprime.H'_alpha_mono (E0_g2h alpha)) => H x y /ltP. move /H; by rewrite /H'_ => /ltP. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)