proposition: Lemma L_succ_ok beta f : nf beta -> S <<= f -> L_spec beta f -> L_spec (succ beta) (fun k => f (S k)).
proof: Proof. intros; apply Large_Sets.L_succ_ok; auto. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)