proposition: Lemma iterate_ge : forall f , S <<= f -> forall j n, j <= iterate f n j.
proof: Proof. induction n. - cbn; auto with arith. - apply Nat.lt_le_incl;rewrite iterate_S_eqn; apply Nat.le_lt_trans with (iterate f n j); auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)