proposition: Lemma F_mono_l alpha beta: E0lt beta alpha -> dominates (F_ alpha) (F_ beta).
proof: Proof. rewrite /dominates; move: (F_mono_l (E0_g2h alpha) (E0_g2h beta)) => H hbeta_alpha. have H' : E0_g2h beta o< E0_g2h alpha by move: hbeta_alpha; rewrite gE0lt_iff. case (H H') => x Hx; exists x; rewrite /dominates_from /F_ => p Hp. apply /ltP; apply : Hx; by apply /leP. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec Arith) hydras(DecPreOrder) hydras(T1 E0) hydras(primRec) hydras(F_alpha F_omega) gaia_hydras(T1Bridge GCanon GHprime)