proposition: Lemma Fake_thm : False.
proof: Proof. assert(F_ E0_omega 2 < F_ 3 2). { rewrite R3, R4. generalize (R6 (F_ 2 2)); intro. generalize (R6 (F_ 2 (F_ 2 2))); intro. lia. } lia. Qed.
imports: hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) Coq(Mult)