proposition: Remark RElim : forall beta n, Canon_plus n alpha beta -> F_ beta n <= F_ alpha n.
proof: Proof. destruct n. - now repeat rewrite F_alpha_0_eq. - intros H; destruct (Canon_plus_first_step_lim Hlim H). + rewrite (F_lim_eqn alpha _). * now rewrite H0. * auto. + rewrite (F_lim_eqn alpha _);auto. destruct (Halpha (Canon alpha (S n))); auto. apply CanonS_lt; now apply Limit_not_Zero. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)