proposition: Lemma mon_iter : forall f, mon f -> geS f -> f 0 <= 1 -> mon (iter f).
proof: Proof. intros f mon_f geS_f f_0. intros n m le. induction le; [now auto|]. simpl. transitivity (S (iter f m)); now auto. Qed.
imports: Arith Lia