proposition: Lemma iterate_mono f (Hf : strict_mono f) (Hf' : S <<= f): forall n, strict_mono (iterate f n).
proof: Proof. induction n. - red; intro i; cbn;auto. - cbn; intros i j H; apply Hf;auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)