proposition: Theorem H'_alpha_gt alpha (Halpha: alpha <> E0zero) n : (n < H'_ alpha n)%N.
proof: Proof. move: (H'_alpha_gt (E0_g2h alpha)) => H. rewrite /H'_ ; apply /ltP; apply H => H0; apply Halpha. apply gE0_eq_intro; case: alpha H H0 Halpha => // ? ? ? H0 ?. injection H0 => Heq; by rewrite -g2h_eqE ?Heq. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)