proposition: Lemma le_sqrt_sqrt_up : forall a, √a <= √°a.
proof: Proof. intros a. unfold sqrt_up. case compare_spec; intros H. - rewrite <- H, sqrt_0. order. - rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le. apply lt_succ_r. now rewrite (lt_succ_pred 0 a H). - now rewrite sqrt_neg. Qed.
imports: NZAxioms NZMulOrder