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.