+
+(* monotonicity *)
+theorem monotonic_sqrt: monotonic nat le sqrt.
+unfold.intros.
+unfold sqrt in ⊢ (? ? (% ?)).
+apply f_m_to_le_max
+ [apply (trans_le ? ? ? ? H).
+ apply le_sqrt_n_n
+ |apply le_to_leb_true.
+ apply (trans_le ? ? ? ? H).
+ apply leq_sqrt_n
+ ]
+qed.
+
+