proposition: Remark R5: forall beta, 3 o<= beta -> beta o< lambda -> forall n, 2 <= n -> forall p, n < p -> exp2 (F_ beta n) <= F_ beta p.
proof: Proof. induction 4. - apply IHlambda; auto. - transitivity (F_ beta m);auto. + apply mono_weak. * apply F_alpha_mono. * auto with arith. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)