proposition: Lemma mon_ge_iter : forall f, mon f -> geS f -> f 0 <= 1 -> forall b, f b <= iter f b.
proof: Proof. intros f mon_f ge_f. induction b; intros; simpl; [now auto|]. apply mon_f. transitivity (f b); [apply ge_f | auto]. Qed.
imports: Arith Lia