proposition: Lemma H'_omega_cube_min : forall k : nat, 0 <> k -> (hyper_exp2 k.+1 <= H'_ (E0_phi0 (E0fin 3)) k)%N.
proof: Proof. move => k Hk; apply /leP; transitivity (Hprime.H'_ (hE0phi0 3) k). - by apply H'_omega_cube_min. - by rewrite /H'_ E0g2h_phi0 E0g2h_Fin. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)