proposition: Fact F3 : (exp2 (exp2 N) <= H'_ (E0_phi0 3 + 3) 0).
proof: Proof. rewrite F2; apply f_minoration. - apply exp2_positive. - apply f_minoration; unfold N. assert (H0 := exp2_gt_id 64). + pose (x:= exp2 64); fold x in H0; fold x; lia. + left. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)