(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/sqrt/".
-
include "nat/times.ma".
include "nat/compare.ma".
include "nat/log.ma".
|simplify;apply le_exp_log;assumption]
|rewrite < H1;simplify;apply le_n]]
qed.
+
+(* 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.
+
+