proposition: Lemma F_alpha_dom alpha: dominates_from 1 (F_ (E0_succ alpha)) (F_ alpha).
proof: Proof. rewrite /dominates_from /F_ g2h_E0_succ => p Hp. apply /ltP; apply F_alpha_dom; 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)