proposition: Lemma iterate_Sge f j : S <<= f -> S <<= iterate f (S j).
proof: Proof. intros h x; rewrite iterate_rw. transitivity (f x). - apply h. - now apply iterate_ge. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)