proposition: Lemma F_mono_l_0 : forall n, Canon_plus (S n) alpha beta -> forall i, (S n < i -> F_ beta i < F_ alpha i)%nat.
proof: Proof. assert (H: E0le (E0_succ beta) alpha) by (now apply Lt_Succ_Le). assert (H0: {alpha = E0_succ beta} + {E0lt (E0_succ beta) alpha}). { rewrite <- lt_Succ_inv in H. apply Lt_Succ_Le in H; destruct (E0.le_lt_eq_dec H); auto. } destruct H0. - intros; apply F2; [trivial | lia]. - intros; eapply F9; eauto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)