proposition: Lemma iterate_mono2 (f: nat -> nat): (forall x y, x <= y -> f x <= f y)%nat -> forall n x y, (x <= y -> iterate f n x <= iterate f n y)%nat.
proof: Proof. induction n. - simpl; trivial. - simpl; intros; now apply H, IHn. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)