Library hydras.solutions_exercises.is_F_monotonous

From hydras Require Import Iterates F_alpha E0.
From Coq Require Import ArithRing Lia Max.
Import Exp2 Canon.
From Coq Require Import Mult.
Open Scope nat_scope.

Section S1.
  Hypothesis H : ∀ (alpha beta:E0), alpha o≤ beta →
                                         ∀ i, 2 ≤ i →
                                                    F_ alpha i ≤ F_ beta i.


  Remark R1 : 3 o≤ E0_omega.

  Remark R2 : 2 ≤ 2.

 Let instance_H := H (E0fin 3) E0_omega R1 _ R2.

  Remark R3 : F_ E0_omega 2 = F_ 2 2.


  Remark R4 : F_ 3 2 = F_ 2 (F_ 2 (F_ 2 2)).

  Remark R6 : ∀ i, i < F_ 2 i.

  Lemma Fake_thm : False.

End S1.