proposition: Lemma sqrt_spec_alt : forall a, 0<=a -> exists r, a == (√a)² + r /\ 0 <= r <= 2*√a.
proof: Proof. intros a Ha. destruct (sqrt_spec _ Ha) as (LE,LT). destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). exists r. split. - now rewrite add_comm. - split. + trivial. + apply (add_le_mono_r _ _ (√a)²). rewrite <- Hr, add_comm. generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc. Qed.
imports: NZAxioms NZMulOrder