proposition: Lemma mono_mono : mono (F_ (S i)).
proof: Proof. intros x y Hxy. repeat rewrite F_S_rw. generalize (iterate_mono _ Hi' (S x)). intro. red in H. specialize (H x y Hxy). apply Nat.lt_le_trans with (iterate (F_ i) (S x) y). auto. clear H. apply iterate_le. auto. auto with arith. Qed.
imports: Coq(ArithRing Lia Arith)