# Library Coq.Numbers.Natural.Abstract.NSqrt

Properties of Square Root Function
Require Import NAxioms NSub NZSqrt.
Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A).
Module Import Private_NZSqrt := Nop <+ NZSqrtProp A A B.
Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
Ltac wrap l := intros; apply l; auto'.
We redefine NZSqrt's results, without the non-negative hyps
Lemma sqrt_spec' : forall a, √ a * √ a <= a < S (√ a) * S (√ a).
Definition sqrt_unique : forall a b, b * b <= a < ( S b )*( S b ) -> √ a == b
:= sqrt_unique.
Lemma sqrt_square : forall a, √( a * a ) == a.
Definition sqrt_le_mono : forall a b, a <= b -> √ a <= √ b
:= sqrt_le_mono.
Definition sqrt_lt_cancel : forall a b, √ a < √ b -> a < b
:= sqrt_lt_cancel.
Lemma sqrt_le_square : forall a b, b * b <= a <-> b <= √ a.
Lemma sqrt_lt_square : forall a b, a < b * b <-> √ a < b.
Definition sqrt_0 := sqrt_0.
Definition sqrt_1 := sqrt_1.
Definition sqrt_2 := sqrt_2.
Definition sqrt_lt_lin : forall a, 1< a -> √ a < a
:= sqrt_lt_lin.
Lemma sqrt_le_lin : forall a, √ a <= a.
Definition sqrt_mul_below : forall a b, √ a * √ b <= √( a * b )
:= sqrt_mul_below.
Lemma sqrt_mul_above : forall a b, √( a * b ) < S (√ a) * S (√ b).
Lemma sqrt_succ_le : forall a, √( S a ) <= S (√ a).
Lemma sqrt_succ_or : forall a, √( S a ) == S (√ a) \/ √( S a ) == √ a.
Definition sqrt_add_le : forall a b, √( a + b ) <= √ a + √ b
:= sqrt_add_le.
Lemma add_sqrt_le : forall a b, √ a + √ b <= √(2*( a + b ) ).
For the moment, we include stuff about sqrt_up with patching them.
Include NZSqrtUpProp A A B Private_NZSqrt.
End NSqrtProp.