proposition: Remark R1: forall n, 2 <= n -> forall p, n < p -> exp2 (F_ alpha n) <= F_ alpha p.
proof: Proof. induction 2. - apply H_alpha; auto. - transitivity (F_ alpha 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)