proposition: Lemma iterate_le_n_Sn (f: nat -> nat): (forall x, x <= f x) -> forall n x, iterate f n x <= iterate f (S n) x.
proof: Proof. induction n /n. - cbn; auto with arith. - cbn; intros; apply h_all_le_x_. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)