proposition: Lemma iterate_le_np_le (f: nat -> nat): (forall x, (x <= f x)%nat) -> forall n p x, (n <= p -> iterate f n x <= iterate f p x)%nat.
proof: Proof. induction 2. - reflexivity. - transitivity (iterate f m x). + assumption. + apply iterate_le_n_Sn, H. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)