proposition: Lemma H'_omega_cube_min k : 0 <> k -> (hyper_exp2 (1 + k) <= H'_ (E0_phi0 3) k)%nat.
proof: Proof. intros H; rewrite H'_omega_cube; unfold hyper_exp2. transitivity (iterate exp2 (1+k) k). - apply iterate_mono2; [ | lia]. intros x y H0; apply mono_weak; auto; apply exp2_mono. - eapply iterate_mono_1 with 1. + apply exp2_mono. + apply exp2_ge_S. + intros n Hn; transitivity (exp2 (S n)). * cbn ; abstract lia. * apply H'_omega_sqr_min; abstract lia. + abstract lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)