proposition: Lemma L4 : exp2 (F_ lambda n) <= F_ lambda (S n).
proof: Proof. repeat rewrite (F_lim_eqn lambda); auto. transitivity (exp2 (F_ (Canon.Canon lambda (S n)) n)). - apply PeanoNat.Nat.lt_le_incl; apply exp2_mono. apply F_mono_l_0 with 0. + apply Paths.Canon_mono1; auto. + apply Paths.Cor12_E0 with (i := 0); auto. * apply Paths.Canon_mono1; auto. * destruct n. -- lia. -- apply (@Paths.KS_thm_2_4_E0 _ Hlambda n0 (S n0)). auto with arith. + auto with arith. - apply R5; auto. + generalize (L04' lambda Hlambda); intro H; specialize (H n). eapply E0.Le_trans with (S n). * rewrite Le_iff. split. -- now compute. -- split. ++ cbn; destruct (Compat815.le_lt_or_eq _ _ Hn). ** apply lt_incl_le; now apply finite_lt. ** subst n; apply Comparable.le_refl. ++ cbn; apply nf_FS. * assumption. + apply Canon.Canon_lt. apply Limit_not_Zero; auto. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)