proposition: Lemma sqrt_up_spec : forall a, 0<a -> (P √°a)² < a <= (√°a)².
proof: Proof. intros a Ha. rewrite sqrt_up_eqn, pred_succ; trivial. assert (Ha' := lt_succ_pred 0 a Ha). rewrite <- Ha' at 3 4. rewrite le_succ_l, lt_succ_r. apply sqrt_spec. now rewrite <- lt_succ_r, Ha'. Qed.
imports: NZAxioms NZMulOrder