proposition: Theorem F_restricted_mono_l alpha : forall beta n, Canon_plus n alpha beta -> F_ beta n <= F_ alpha n.
proof: Proof. now destruct (TH_packed alpha). Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)