proposition: Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a).
proof: Proof. intros a. unfold sqrt_up. case compare_spec; intros H; try apply le_le_succ_r, sqrt_nonneg. rewrite <- succ_le_mono. apply sqrt_le_mono. rewrite <- (lt_succ_pred 0 a H) at 2. apply le_succ_diag_r. Qed.
imports: NZAxioms NZMulOrder