proposition: Lemma iterate_le f (Hf : mono f) : forall x y, x <= y -> forall z, iterate f x z <= iterate f y z.
proof: Proof. induction 1. auto. intros. rewrite iterate_S_eqn. transitivity (iterate f m z); auto. apply mono_le. auto. Qed.
imports: Coq(ArithRing Lia Arith)