proposition: Lemma LF2' i: (1 <= i)%N -> (Exp2.exp2 i < F_ (E0fin 2) i)%N.
proof: Proof. move => Hi; apply /ltP; replace (F_ (E0fin 2) i) with (F_alpha.F_ (hE0fin 2) i). - apply LF2'; by apply /leP. - rewrite /F_; congr hF_; by apply E0_eq_intro . Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec Arith) hydras(DecPreOrder) hydras(T1 E0) hydras(primRec) hydras(F_alpha F_omega) gaia_hydras(T1Bridge GCanon GHprime)