Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Square Root Function

Require Import NZAxioms NZMulOrder.

Interface of a sqrt function, then its specification on naturals

Module Type Sqrt (Import A : Typ).
 Parameter Inline sqrt : t -> t.
End Sqrt.

Module Type SqrtNotation (A : Typ)(Import B : Sqrt A).
 Notation "√ x" := (sqrt x) (at level 6).
End SqrtNotation.

Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.

Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
 Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a).
 Axiom sqrt_neg : forall a, a<0 -> √a == 0.
End NZSqrtSpec.

Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A.
Module Type NZSqrt' (A : NZOrdAxiomsSig) := Sqrt' A <+ NZSqrtSpec A.

Derived properties of power

Module Type NZSqrtProp
 (Import A : NZOrdAxiomsSig')
 (Import B : NZSqrt' A)
 (Import C : NZMulOrderProp A).

Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²").

First, sqrt is non-negative

Lemma sqrt_spec_nonneg : forall b,
 b² < (S b)² -> 0 <= b.forall b : t, b² < (S b)² -> 0 <= b
Proof.forall b : t, b² < (S b)² -> 0 <= b
 intros b LT.b:t
LT:b² < (S b)²
0 <= b
 destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial.b:t
LT:b² < (S b)²
Hb:b < 0
0 <= b exfalso.b:t
LT:b² < (S b)²
Hb:b < 0
False
 assert ((S b)² < b²).b:t
LT:b² < (S b)²
Hb:b < 0
(S b)² < b²
b:t
LT:b² < (S b)²
Hb:b < 0
H:(S b)² < b²
False
 -b:t
LT:b² < (S b)²
Hb:b < 0
(S b)² < b² rewrite mul_succ_l, <- (add_0_r b²).b:t
LT:b² < (S b)²
Hb:b < 0
b * S b + S b < b² + 0
   apply add_lt_le_mono.b:t
LT:b² < (S b)²
Hb:b < 0
b * S b < b²
b:t
LT:b² < (S b)²
Hb:b < 0
S b <= 0
   +b:t
LT:b² < (S b)²
Hb:b < 0
b * S b < b² apply mul_lt_mono_neg_l; trivial.b:t
LT:b² < (S b)²
Hb:b < 0
b < S b apply lt_succ_diag_r.
   +b:t
LT:b² < (S b)²
Hb:b < 0
S b <= 0 now apply le_succ_l.
 -b:t
LT:b² < (S b)²
Hb:b < 0
H:(S b)² < b²
False order.
Qed.

Lemma sqrt_nonneg : forall a, 0<=√a.forall a : t, 0 <= √ a
Proof.forall a : t, 0 <= √ a
 intros.a:t
0 <= √ a destruct (lt_ge_cases a 0) as [Ha|Ha].a:t
Ha:a < 0
0 <= √ a
a:t
Ha:0 <= a
0 <= √ a
 -a:t
Ha:a < 0
0 <= √ a now rewrite (sqrt_neg _ Ha).
 -a:t
Ha:0 <= a
0 <= √ a apply sqrt_spec_nonneg.a:t
Ha:0 <= a
(√ a)² < (S √ a)² destruct (sqrt_spec a Ha).a:t
Ha:0 <= a
H:(√ a)² <= a
H0:a < (S √ a)²
(√ a)² < (S √ a)² order.
Qed.

The spec of sqrt indeed determines it

Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b.forall a b : t, b² <= a < (S b)² -> √ a == b
Proof.forall a b : t, b² <= a < (S b)² -> √ a == b
 intros a b (LEb,LTb).a, b:t
LEb:b² <= a
LTb:a < (S b)²
√ a == b
 assert (Ha : 0<=a) by (transitivity (b²); trivial using square_nonneg).a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
√ a == b
 assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order).a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
√ a == b
 assert (Ha': 0<=√a) by now apply sqrt_nonneg.a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
√ a == b
 destruct (sqrt_spec a Ha) as (LEa,LTa).a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
√ a == b
 assert (b <= √a).a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
b <= √ a
a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
√ a == b
 -a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
b <= √ a apply lt_succ_r, square_lt_simpl_nonneg; [|order].a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
0 <= S √ a
   now apply lt_le_incl, lt_succ_r.
 -a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
√ a == b assert (√a <= b).a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
√ a <= b
a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
H0:√ a <= b
√ a == b
   +a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
√ a <= b apply lt_succ_r, square_lt_simpl_nonneg; [|order].a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
0 <= S b
     now apply lt_le_incl, lt_succ_r.
   +a, b:t
LEb:b² <= a
LTb:a < (S b)²
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
LEa:(√ a)² <= a
LTa:a < (S √ a)²
H:b <= √ a
H0:√ a <= b
√ a == b order.
Qed.

Hence sqrt is a morphism

Instance sqrt_wd : Proper (eq==>eq) sqrt.Proper (eq ==> eq) sqrt
Proof.Proper (eq ==> eq) sqrt
 intros x x' Hx.x, x':t
Hx:x == x'
√ x == √ x'
 destruct (lt_ge_cases x 0) as [H|H].x, x':t
Hx:x == x'
H:x < 0
√ x == √ x'
x, x':t
Hx:x == x'
H:0 <= x
√ x == √ x'
 -x, x':t
Hx:x == x'
H:x < 0
√ x == √ x' rewrite 2 sqrt_neg; trivial.x, x':t
Hx:x == x'
H:x < 0
0 == 0
x, x':t
Hx:x == x'
H:x < 0
x' < 0 +x, x':t
Hx:x == x'
H:x < 0
0 == 0 reflexivity.
   +x, x':t
Hx:x == x'
H:x < 0
x' < 0 now rewrite <- Hx.
 -x, x':t
Hx:x == x'
H:0 <= x
√ x == √ x' apply sqrt_unique.x, x':t
Hx:x == x'
H:0 <= x
(√ x')² <= x < (S √ x')² rewrite Hx in *.x, x':t
Hx:x == x'
H:0 <= x'
(√ x')² <= x' < (S √ x')² now apply sqrt_spec.
Qed.

An alternate specification

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

Lemma sqrt_unique' : forall a b c, 0<=c<=2*b ->
 a == b² + c -> √a == b.forall a b c : t,
0 <= c <= 2 * b -> a == b² + c -> √ a == b
Proof.forall a b c : t,
0 <= c <= 2 * b -> a == b² + c -> √ a == b
 intros a b c (Hc,H) EQ.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
√ a == b
 apply sqrt_unique.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² <= a < (S b)²
 rewrite EQ.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² <= b² + c < (S b)²
 split.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² <= b² + c
a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² + c < (S b)²
 -a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² <= b² + c rewrite <- add_0_r at 1.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² + 0 <= b² + c now apply add_le_mono_l.
 -a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² + c < (S b)² nzsimpl.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² + c < S (b² + b + b) apply lt_succ_r.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² + c <= b² + b + b
   rewrite <- add_assoc.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
b² + c <= b² + (b + b) apply add_le_mono_l.a, b, c:t
Hc:0 <= c
H:c <= 2 * b
EQ:a == b² + c
c <= b + b
   generalize H; now nzsimpl'.
Qed.

Sqrt is exact on squares

Lemma sqrt_square : forall a, 0<=a -> √(a²) == a.forall a : t, 0 <= a -> √ a² == a
Proof.forall a : t, 0 <= a -> √ a² == a
 intros a Ha.a:t
Ha:0 <= a
√ a² == a
 apply sqrt_unique' with 0.a:t
Ha:0 <= a
0 <= 0 <= 2 * a
a:t
Ha:0 <= a
a² == a² + 0
 -a:t
Ha:0 <= a
0 <= 0 <= 2 * a split.a:t
Ha:0 <= a
0 <= 0
a:t
Ha:0 <= a
0 <= 2 * a +a:t
Ha:0 <= a
0 <= 0 order. +a:t
Ha:0 <= a
0 <= 2 * a apply mul_nonneg_nonneg; order'. -a:t
Ha:0 <= a
a² == a² + 0 now nzsimpl.
Qed.

Sqrt and predecessors of squares

Lemma sqrt_pred_square : forall a, 0<a -> √(P a²) == P a.forall a : t, 0 < a -> √ (P a²) == P a
Proof.forall a : t, 0 < a -> √ (P a²) == P a
 intros a Ha.a:t
Ha:0 < a
√ (P a²) == P a
 apply sqrt_unique.a:t
Ha:0 < a
(P a)² <= P a² < (S (P a))²
 assert (EQ := lt_succ_pred 0 a Ha).a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² <= P a² < (S (P a))²
 rewrite EQ.a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² <= P a² < a² split.a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² <= P a²
a:t
Ha:0 < a
EQ:S (P a) == a
P a² < a²
 -a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² <= P a² apply lt_succ_r.a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² < S (P a²)
   rewrite (lt_succ_pred 0).a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² < a²
a:t
Ha:0 < a
EQ:S (P a) == a
0 < a²
   +a:t
Ha:0 < a
EQ:S (P a) == a
(P a)² < a² assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ).a:t
Ha:0 < a
EQ:S (P a) == a
H:0 <= P a
(P a)² < a²
     assert (P a < a) by (now rewrite <- le_succ_l, EQ).a:t
Ha:0 < a
EQ:S (P a) == a
H:0 <= P a
H0:P a < a
(P a)² < a²
     apply mul_lt_mono_nonneg; trivial.
   +a:t
Ha:0 < a
EQ:S (P a) == a
0 < a² now apply mul_pos_pos.
 -a:t
Ha:0 < a
EQ:S (P a) == a
P a² < a² apply le_succ_l.a:t
Ha:0 < a
EQ:S (P a) == a
S (P a²) <= a²
   rewrite (lt_succ_pred 0).a:t
Ha:0 < a
EQ:S (P a) == a
a² <= a²
a:t
Ha:0 < a
EQ:S (P a) == a
0 < a² +a:t
Ha:0 < a
EQ:S (P a) == a
a² <= a² reflexivity. +a:t
Ha:0 < a
EQ:S (P a) == a
0 < a² now apply mul_pos_pos.
Qed.

Sqrt is a monotone function (but not a strict one)

Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b.forall a b : t, a <= b -> √ a <= √ b
Proof.forall a b : t, a <= b -> √ a <= √ b
 intros a b Hab.a, b:t
Hab:a <= b
√ a <= √ b
 destruct (lt_ge_cases a 0) as [Ha|Ha].a, b:t
Hab:a <= b
Ha:a < 0
√ a <= √ b
a, b:t
Hab:a <= b
Ha:0 <= a
√ a <= √ b
 -a, b:t
Hab:a <= b
Ha:a < 0
√ a <= √ b rewrite (sqrt_neg _ Ha).a, b:t
Hab:a <= b
Ha:a < 0
0 <= √ b apply sqrt_nonneg.
 -a, b:t
Hab:a <= b
Ha:0 <= a
√ a <= √ b assert (Hb : 0 <= b) by order.a, b:t
Hab:a <= b
Ha:0 <= a
Hb:0 <= b
√ a <= √ b
   destruct (sqrt_spec a Ha) as (LE,_).a, b:t
Hab:a <= b
Ha:0 <= a
Hb:0 <= b
LE:(√ a)² <= a
√ a <= √ b
   destruct (sqrt_spec b Hb) as (_,LT).a, b:t
Hab:a <= b
Ha:0 <= a
Hb:0 <= b
LE:(√ a)² <= a
LT:b < (S √ b)²
√ a <= √ b
   apply lt_succ_r.a, b:t
Hab:a <= b
Ha:0 <= a
Hb:0 <= b
LE:(√ a)² <= a
LT:b < (S √ b)²
√ a < S √ b
   apply square_lt_simpl_nonneg; try order.a, b:t
Hab:a <= b
Ha:0 <= a
Hb:0 <= b
LE:(√ a)² <= a
LT:b < (S √ b)²
0 <= S √ b
   now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
Qed.

No reverse result for <=, consider for instance √2 <= √1

Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.forall a b : t, √ a < √ b -> a < b
Proof.forall a b : t, √ a < √ b -> a < b
 intros a b H.a, b:t
H:√ a < √ b
a < b
 destruct (lt_ge_cases b 0) as [Hb|Hb].a, b:t
H:√ a < √ b
Hb:b < 0
a < b
a, b:t
H:√ a < √ b
Hb:0 <= b
a < b
 -a, b:t
H:√ a < √ b
Hb:b < 0
a < b rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order.
 -a, b:t
H:√ a < √ b
Hb:0 <= b
a < b destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|].a, b:t
H:√ a < √ b
Hb:0 <= b
Ha:0 <= a
a < b
   destruct (sqrt_spec a Ha) as (_,LT).a, b:t
H:√ a < √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
a < b
   destruct (sqrt_spec b Hb) as (LE,_).a, b:t
H:√ a < √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
a < b
   apply le_succ_l in H.a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
a < b
   assert ((S (√a))² <= (√b)²).a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
(S √ a)² <= (√ b)²
a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
H0:(S √ a)² <= (√ b)²
a < b
   +a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
(S √ a)² <= (√ b)² apply mul_le_mono_nonneg; trivial.a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
0 <= S √ a
a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
0 <= S √ a
     *a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
0 <= S √ a now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
     *a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
0 <= S √ a now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
   +a, b:t
H:S √ a <= √ b
Hb:0 <= b
Ha:0 <= a
LT:a < (S √ a)²
LE:(√ b)² <= b
H0:(S √ a)² <= (√ b)²
a < b order.
Qed.

When left side is a square, we have an equivalence for <=

Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a).forall a b : t,
0 <= a -> 0 <= b -> b² <= a <-> b <= √ a
Proof.forall a b : t,
0 <= a -> 0 <= b -> b² <= a <-> b <= √ a
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
b² <= a <-> b <= √ a split; intros H.a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² <= a
b <= √ a
a, b:t
Ha:0 <= a
Hb:0 <= b
H:b <= √ a
b² <= a
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² <= a
b <= √ a rewrite <- (sqrt_square b); trivial.a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² <= a
√ b² <= √ a
   now apply sqrt_le_mono.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:b <= √ a
b² <= a destruct (sqrt_spec a Ha) as (LE,LT).a, b:t
Ha:0 <= a
Hb:0 <= b
H:b <= √ a
LE:(√ a)² <= a
LT:a < (S √ a)²
b² <= a
   transitivity (√a)²; trivial.a, b:t
Ha:0 <= a
Hb:0 <= b
H:b <= √ a
LE:(√ a)² <= a
LT:a < (S √ a)²
b² <= (√ a)²
   now apply mul_le_mono_nonneg.
Qed.

When right side is a square, we have an equivalence for <

Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b).forall a b : t, 0 <= a -> 0 <= b -> a < b² <-> √ a < b
Proof.forall a b : t, 0 <= a -> 0 <= b -> a < b² <-> √ a < b
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
a < b² <-> √ a < b split; intros H.a, b:t
Ha:0 <= a
Hb:0 <= b
H:a < b²
√ a < b
a, b:t
Ha:0 <= a
Hb:0 <= b
H:√ a < b
a < b²
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:a < b²
√ a < b destruct (sqrt_spec a Ha) as (LE,_).a, b:t
Ha:0 <= a
Hb:0 <= b
H:a < b²
LE:(√ a)² <= a
√ a < b
   apply square_lt_simpl_nonneg; try order.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:√ a < b
a < b² rewrite <- (sqrt_square b Hb) in H.a, b:t
Ha:0 <= a
Hb:0 <= b
H:√ a < √ b²
a < b²
   now apply sqrt_lt_cancel.
Qed.

Sqrt and basic constants

Lemma sqrt_0 : √0 == 0.√ 0 == 0
Proof.√ 0 == 0
 rewrite <- (mul_0_l 0) at 1.√ 0² == 0 now apply sqrt_square.
Qed.

Lemma sqrt_1 : √1 == 1.√ 1 == 1
Proof.√ 1 == 1
 rewrite <- (mul_1_l 1) at 1.√ 1² == 1 apply sqrt_square.0 <= 1 order'.
Qed.

Lemma sqrt_2 : √2 == 1.√ 2 == 1
Proof.√ 2 == 1
  apply sqrt_unique' with 1.0 <= 1 <= 2 * 1
2 == 1² + 1 -0 <= 1 <= 2 * 1 nzsimpl; split; order'. -2 == 1² + 1 now nzsimpl'.
Qed.

Lemma sqrt_pos : forall a, 0 < √a <-> 0 < a.forall a : t, 0 < √ a <-> 0 < a
Proof.forall a : t, 0 < √ a <-> 0 < a
  intros a.a:t
0 < √ a <-> 0 < a split; intros Ha.a:t
Ha:0 < √ a
0 < a
a:t
Ha:0 < a
0 < √ a -a:t
Ha:0 < √ a
0 < a apply sqrt_lt_cancel.a:t
Ha:0 < √ a
√ 0 < √ a now rewrite sqrt_0.
  -a:t
Ha:0 < a
0 < √ a rewrite <- le_succ_l, <- one_succ, <- sqrt_1.a:t
Ha:0 < a
√ 1 <= √ a apply sqrt_le_mono.a:t
Ha:0 < a
1 <= a
    now rewrite one_succ, le_succ_l.
Qed.

Lemma sqrt_lt_lin : forall a, 1<a -> √a<a.forall a : t, 1 < a -> √ a < a
Proof.forall a : t, 1 < a -> √ a < a
 intros a Ha.a:t
Ha:1 < a
√ a < a rewrite <- sqrt_lt_square; try order'.a:t
Ha:1 < a
a < a²
 rewrite <- (mul_1_r a) at 1.a:t
Ha:1 < a
a * 1 < a²
 rewrite <- mul_lt_mono_pos_l; order'.
Qed.

Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.forall a : t, 0 <= a -> √ a <= a
Proof.forall a : t, 0 <= a -> √ a <= a
 intros a Ha.a:t
Ha:0 <= a
√ a <= a
 destruct (le_gt_cases a 0) as [H|H].a:t
Ha:0 <= a
H:a <= 0
√ a <= a
a:t
Ha:0 <= a
H:0 < a
√ a <= a
 -a:t
Ha:0 <= a
H:a <= 0
√ a <= a setoid_replace a with 0 by order.a:t
Ha:0 <= a
H:a <= 0
√ 0 <= 0 now rewrite sqrt_0.
 -a:t
Ha:0 <= a
H:0 < a
√ a <= a destruct (le_gt_cases a 1) as [H'|H'].a:t
Ha:0 <= a
H:0 < a
H':a <= 1
√ a <= a
a:t
Ha:0 <= a
H:0 < a
H':1 < a
√ a <= a
   +a:t
Ha:0 <= a
H:0 < a
H':a <= 1
√ a <= a rewrite <- le_succ_l, <- one_succ in H.a:t
Ha:0 <= a
H:1 <= a
H':a <= 1
√ a <= a
     setoid_replace a with 1 by order.a:t
Ha:0 <= a
H:1 <= a
H':a <= 1
√ 1 <= 1 now rewrite sqrt_1.
   +a:t
Ha:0 <= a
H:0 < a
H':1 < a
√ a <= a now apply lt_le_incl, sqrt_lt_lin.
Qed.

Sqrt and multiplication.

Due to rounding error, we don't have the usual √(a*b) = √a*√b but only lower and upper bounds.

Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).forall a b : t, √ a * √ b <= √ (a * b)
Proof.forall a b : t, √ a * √ b <= √ (a * b)
 intros a b.a, b:t
√ a * √ b <= √ (a * b)
 destruct (lt_ge_cases a 0) as [Ha|Ha].a, b:t
Ha:a < 0
√ a * √ b <= √ (a * b)
a, b:t
Ha:0 <= a
√ a * √ b <= √ (a * b)
 -a, b:t
Ha:a < 0
√ a * √ b <= √ (a * b) rewrite (sqrt_neg a Ha).a, b:t
Ha:a < 0
0 * √ b <= √ (a * b) nzsimpl.a, b:t
Ha:a < 0
0 <= √ (a * b) apply sqrt_nonneg.
 -a, b:t
Ha:0 <= a
√ a * √ b <= √ (a * b) destruct (lt_ge_cases b 0) as [Hb|Hb].a, b:t
Ha:0 <= a
Hb:b < 0
√ a * √ b <= √ (a * b)
a, b:t
Ha:0 <= a
Hb:0 <= b
√ a * √ b <= √ (a * b)
   +a, b:t
Ha:0 <= a
Hb:b < 0
√ a * √ b <= √ (a * b) rewrite (sqrt_neg b Hb).a, b:t
Ha:0 <= a
Hb:b < 0
√ a * 0 <= √ (a * b) nzsimpl.a, b:t
Ha:0 <= a
Hb:b < 0
0 <= √ (a * b) apply sqrt_nonneg.
   +a, b:t
Ha:0 <= a
Hb:0 <= b
√ a * √ b <= √ (a * b) assert (Ha':=sqrt_nonneg a).a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
√ a * √ b <= √ (a * b)
     assert (Hb':=sqrt_nonneg b).a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
√ a * √ b <= √ (a * b)
     apply sqrt_le_square; try now apply mul_nonneg_nonneg.a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a * √ b)² <= a * b
     rewrite mul_shuffle1.a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² * (√ b)² <= a * b
     apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg.a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² <= a
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ b)² <= b
     *a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² <= a now apply sqrt_spec.
     *a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ b)² <= b now apply sqrt_spec.
Qed.

Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b).forall a b : t,
0 <= a -> 0 <= b -> √ (a * b) < S √ a * S √ b
Proof.forall a b : t,
0 <= a -> 0 <= b -> √ (a * b) < S √ a * S √ b
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
√ (a * b) < S √ a * S √ b
 apply sqrt_lt_square.a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a * b
a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= S √ a * S √ b
a, b:t
Ha:0 <= a
Hb:0 <= b
a * b < (S √ a * S √ b)²
 -a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a * b now apply mul_nonneg_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= S √ a * S √ b apply mul_nonneg_nonneg.a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= S √ a
a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= S √ b
   +a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= S √ a now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
   +a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= S √ b now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
a * b < (S √ a * S √ b)² rewrite mul_shuffle1.a, b:t
Ha:0 <= a
Hb:0 <= b
a * b < (S √ a)² * (S √ b)²
   apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec.
Qed.

And we can't find better approximations in general.

The lower bound is exact for squares
Concerning the upper bound, for any c>0, take a=b=c²-1, then √(a*b) = c² -1 while S √a = S √b = c

Sqrt and successor :

the sqrt function climbs by at most 1 at a time
otherwise it stays at the same value
the +1 steps occur for squares

Lemma sqrt_succ_le : forall a, 0<=a -> √(S a) <= S (√a).forall a : t, 0 <= a -> √ (S a) <= S √ a
Proof.forall a : t, 0 <= a -> √ (S a) <= S √ a
 intros a Ha.a:t
Ha:0 <= a
√ (S a) <= S √ a
 apply lt_succ_r.a:t
Ha:0 <= a
√ (S a) < S (S √ a)
 apply sqrt_lt_square.a:t
Ha:0 <= a
0 <= S a
a:t
Ha:0 <= a
0 <= S (S √ a)
a:t
Ha:0 <= a
S a < (S (S √ a))²
 -a:t
Ha:0 <= a
0 <= S a now apply le_le_succ_r.
 -a:t
Ha:0 <= a
0 <= S (S √ a) apply le_le_succ_r, le_le_succ_r, sqrt_nonneg.
 -a:t
Ha:0 <= a
S a < (S (S √ a))² rewrite <- (add_1_l (S (√a))).a:t
Ha:0 <= a
S a < (1 + S √ a)²
   apply lt_le_trans with (1²+(S (√a))²).a:t
Ha:0 <= a
S a < 1² + (S √ a)²
a:t
Ha:0 <= a
1² + (S √ a)² <= (1 + S √ a)²
   +a:t
Ha:0 <= a
S a < 1² + (S √ a)² rewrite mul_1_l, add_1_l, <- succ_lt_mono.a:t
Ha:0 <= a
a < (S √ a)²
     now apply sqrt_spec.
   +a:t
Ha:0 <= a
1² + (S √ a)² <= (1 + S √ a)² apply add_square_le.a:t
Ha:0 <= a
0 <= 1
a:t
Ha:0 <= a
0 <= S √ a *a:t
Ha:0 <= a
0 <= 1 order'. *a:t
Ha:0 <= a
0 <= S √ a apply le_le_succ_r, sqrt_nonneg.
Qed.

Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a.forall a : t,
0 <= a -> √ (S a) == S √ a \/ √ (S a) == √ a
Proof.forall a : t,
0 <= a -> √ (S a) == S √ a \/ √ (S a) == √ a
 intros a Ha.a:t
Ha:0 <= a
√ (S a) == S √ a \/ √ (S a) == √ a
 destruct (le_gt_cases (√(S a)) (√a)) as [H|H].a:t
Ha:0 <= a
H:√ (S a) <= √ a
√ (S a) == S √ a \/ √ (S a) == √ a
a:t
Ha:0 <= a
H:√ a < √ (S a)
√ (S a) == S √ a \/ √ (S a) == √ a
 -a:t
Ha:0 <= a
H:√ (S a) <= √ a
√ (S a) == S √ a \/ √ (S a) == √ a right.a:t
Ha:0 <= a
H:√ (S a) <= √ a
√ (S a) == √ a generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order.
 -a:t
Ha:0 <= a
H:√ a < √ (S a)
√ (S a) == S √ a \/ √ (S a) == √ a left.a:t
Ha:0 <= a
H:√ a < √ (S a)
√ (S a) == S √ a apply le_succ_l in H.a:t
Ha:0 <= a
H:S √ a <= √ (S a)
√ (S a) == S √ a generalize (sqrt_succ_le a Ha); order.
Qed.

Lemma sqrt_eq_succ_iff_square : forall a, 0<=a ->
 (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²).forall a : t,
0 <= a ->
√ (S a) == S √ a <->
(exists b : t, 0 < b /\ S a == b²)
Proof.forall a : t,
0 <= a ->
√ (S a) == S √ a <->
(exists b : t, 0 < b /\ S a == b²)
 intros a Ha.a:t
Ha:0 <= a
√ (S a) == S √ a <->
(exists b : t, 0 < b /\ S a == b²) split.a:t
Ha:0 <= a
√ (S a) == S √ a -> exists b : t, 0 < b /\ S a == b²
a:t
Ha:0 <= a
(exists b : t, 0 < b /\ S a == b²) -> √ (S a) == S √ a
 -a:t
Ha:0 <= a
√ (S a) == S √ a -> exists b : t, 0 < b /\ S a == b² intros EQ.a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
exists b : t, 0 < b /\ S a == b² exists (S (√a)).a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
0 < S √ a /\ S a == (S √ a)²
   split.a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
0 < S √ a
a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
S a == (S √ a)² +a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
0 < S √ a apply lt_succ_r, sqrt_nonneg.
   +a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
S a == (S √ a)² generalize (proj2 (sqrt_spec a Ha)).a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
a < (S √ a)² -> S a == (S √ a)² rewrite <- le_succ_l.a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
S a <= (S √ a)² -> S a == (S √ a)²
     assert (Ha' : 0 <= S a) by now apply le_le_succ_r.a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
Ha':0 <= S a
S a <= (S √ a)² -> S a == (S √ a)²
     generalize (proj1 (sqrt_spec (S a) Ha')).a:t
Ha:0 <= a
EQ:√ (S a) == S √ a
Ha':0 <= S a
(√ (S a))² <= S a ->
S a <= (S √ a)² -> S a == (S √ a)² rewrite EQ; order.
 -a:t
Ha:0 <= a
(exists b : t, 0 < b /\ S a == b²) -> √ (S a) == S √ a intros (b & Hb & H).a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
√ (S a) == S √ a
   rewrite H.a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
√ b² == S √ a rewrite sqrt_square; try order.a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
b == S √ a
   symmetry.a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
S √ a == b
   rewrite <- (lt_succ_pred 0 b Hb).a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
S √ a == S (P b) f_equiv.a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
√ a == P b
   rewrite <- (lt_succ_pred 0 b²) in H.a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == S (P b²)
√ a == P b
a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
0 < b² +a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == S (P b²)
√ a == P b apply succ_inj in H.a:t
Ha:0 <= a
b:t
Hb:0 < b
H:a == P b²
√ a == P b
                                         now rewrite H, sqrt_pred_square.
   +a:t
Ha:0 <= a
b:t
Hb:0 < b
H:S a == b²
0 < b² now apply mul_pos_pos.
Qed.

Sqrt and addition

Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.forall a b : t, √ (a + b) <= √ a + √ b
Proof.forall a b : t, √ (a + b) <= √ a + √ b
  assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b).forall a b : t, a < 0 -> √ (a + b) <= √ a + √ b
AUX:forall a b : t, a < 0 -> √ (a + b) <= √ a + √ b
forall a b : t, √ (a + b) <= √ a + √ b
  -forall a b : t, a < 0 -> √ (a + b) <= √ a + √ b intros a b Ha.a, b:t
Ha:a < 0
√ (a + b) <= √ a + √ b rewrite (sqrt_neg a Ha).a, b:t
Ha:a < 0
√ (a + b) <= 0 + √ b nzsimpl.a, b:t
Ha:a < 0
√ (a + b) <= √ b
    apply sqrt_le_mono.a, b:t
Ha:a < 0
a + b <= b
    rewrite <- (add_0_l b) at 2.a, b:t
Ha:a < 0
a + b <= 0 + b
    apply add_le_mono_r; order.
  -AUX:forall a b : t, a < 0 -> √ (a + b) <= √ a + √ b
forall a b : t, √ (a + b) <= √ a + √ b intros a b.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
√ (a + b) <= √ a + √ b
    destruct (lt_ge_cases a 0) as [Ha|Ha].AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:a < 0
√ (a + b) <= √ a + √ b
AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
√ (a + b) <= √ a + √ b +AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:a < 0
√ (a + b) <= √ a + √ b now apply AUX.
    +AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
√ (a + b) <= √ a + √ b destruct (lt_ge_cases b 0) as [Hb|Hb].AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:b < 0
√ (a + b) <= √ a + √ b
AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
√ (a + b) <= √ a + √ b
      *AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:b < 0
√ (a + b) <= √ a + √ b rewrite (add_comm a), (add_comm (√a)); now apply AUX.
      *AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
√ (a + b) <= √ a + √ b assert (Ha':=sqrt_nonneg a).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
√ (a + b) <= √ a + √ b
        assert (Hb':=sqrt_nonneg b).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
√ (a + b) <= √ a + √ b
        rewrite <- lt_succ_r.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
√ (a + b) < S (√ a + √ b)
        apply sqrt_lt_square.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= a + b
AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= S (√ a + √ b)
AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
a + b < (S (√ a + √ b))²
        --AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= a + b now apply add_nonneg_nonneg.
        --AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= S (√ a + √ b) now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg.
        --AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
a + b < (S (√ a + √ b))² destruct (sqrt_spec a Ha) as (_,LTa).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
LTa:a < (S √ a)²
a + b < (S (√ a + √ b))²
           destruct (sqrt_spec b Hb) as (_,LTb).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
LTa:a < (S √ a)²
LTb:b < (S √ b)²
a + b < (S (√ a + √ b))²
           revert LTa LTb.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
a < (S √ a)² ->
b < (S √ b)² -> a + b < (S (√ a + √ b))² nzsimpl.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
a < S ((√ a)² + √ a + √ a) ->
b < S ((√ b)² + √ b + √ b) ->
a + b < S ((√ a + √ b)² + (√ a + √ b) + (√ a + √ b)) rewrite 3 lt_succ_r.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
a <= (√ a)² + √ a + √ a ->
b <= (√ b)² + √ b + √ b ->
a + b <= (√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           intros LTa LTb.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
LTa:a <= (√ a)² + √ a + √ a
LTb:b <= (√ b)² + √ b + √ b
a + b <= (√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           assert (H:=add_le_mono _ _ _ _ LTa LTb).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
LTa:a <= (√ a)² + √ a + √ a
LTb:b <= (√ b)² + √ b + √ b
H:a + b <= (√ a)² + √ a + √ a + ((√ b)² + √ b + √ b)
a + b <= (√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           etransitivity; [eexact H|].AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
LTa:a <= (√ a)² + √ a + √ a
LTb:b <= (√ b)² + √ b + √ b
H:a + b <= (√ a)² + √ a + √ a + ((√ b)² + √ b + √ b)
(√ a)² + √ a + √ a + ((√ b)² + √ b + √ b) <=
(√ a + √ b)² + (√ a + √ b) + (√ a + √ b) clear LTa LTb H.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + √ a + √ a + ((√ b)² + √ b + √ b) <=
(√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           rewrite <- (add_assoc _ (√a) (√a)).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ a + √ a) + ((√ b)² + √ b + √ b) <=
(√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           rewrite <- (add_assoc _ (√b) (√b)).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ a + √ a) + ((√ b)² + (√ b + √ b)) <=
(√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           rewrite add_shuffle1.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ b)² + (√ a + √ a + (√ b + √ b)) <=
(√ a + √ b)² + (√ a + √ b) + (√ a + √ b)
           rewrite <- (add_assoc _ (√a + √b)).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ b)² + (√ a + √ a + (√ b + √ b)) <=
(√ a + √ b)² + (√ a + √ b + (√ a + √ b))
           rewrite (add_shuffle1 (√a) (√b)).AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ b)² + (√ a + √ a + (√ b + √ b)) <=
(√ a + √ b)² + (√ a + √ a + (√ b + √ b))
           apply add_le_mono_r.AUX:forall a0 b0 : t, a0 < 0 -> √ (a0 + b0) <= √ a0 + √ b0
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ b)² <= (√ a + √ b)²
           now apply add_square_le.
Qed.

convexity inequality for sqrt: sqrt of middle is above middle of square roots.

Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)).forall a b : t,
0 <= a -> 0 <= b -> √ a + √ b <= √ (2 * (a + b))
Proof.forall a b : t,
0 <= a -> 0 <= b -> √ a + √ b <= √ (2 * (a + b))
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
√ a + √ b <= √ (2 * (a + b))
 assert (Ha':=sqrt_nonneg a).a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
√ a + √ b <= √ (2 * (a + b))
 assert (Hb':=sqrt_nonneg b).a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
√ a + √ b <= √ (2 * (a + b))
 apply sqrt_le_square.a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= 2 * (a + b)
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= √ a + √ b
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a + √ b)² <= 2 * (a + b)
 -a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= 2 * (a + b) apply mul_nonneg_nonneg.a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= 2
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= a + b +a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= 2 order'. +a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= a + b now apply add_nonneg_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= √ a + √ b now apply add_nonneg_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a + √ b)² <= 2 * (a + b) transitivity (2*((√a)² + (√b)²)).a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a + √ b)² <= 2 * ((√ a)² + (√ b)²)
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
2 * ((√ a)² + (√ b)²) <= 2 * (a + b)
   +a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a + √ b)² <= 2 * ((√ a)² + (√ b)²) now apply square_add_le.
   +a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
2 * ((√ a)² + (√ b)²) <= 2 * (a + b) apply mul_le_mono_nonneg_l.a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= 2
a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ b)² <= a + b *a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
0 <= 2 order'.
     *a, b:t
Ha:0 <= a
Hb:0 <= b
Ha':0 <= √ a
Hb':0 <= √ b
(√ a)² + (√ b)² <= a + b apply add_le_mono; now apply sqrt_spec.
Qed.

End NZSqrtProp.

Module Type NZSqrtUpProp
 (Import A : NZDecOrdAxiomsSig')
 (Import B : NZSqrt' A)
 (Import C : NZMulOrderProp A)
 (Import D : NZSqrtProp A B C).

sqrt_up : a square root that rounds up instead of down

Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²").

For once, we define instead of axiomatizing, thanks to sqrt

Definition sqrt_up a :=
 match compare 0 a with
  | Lt => S √(P a)
  | _ => 0
 end.

Local Notation "√° a" := (sqrt_up a) (at level 6, no associativity).

Lemma sqrt_up_eqn0 : forall a, a<=0 -> √°a == 0.forall a : t, a <= 0 -> √° a == 0
Proof.forall a : t, a <= 0 -> √° a == 0
 intros a Ha.a:t
Ha:a <= 0
√° a == 0 unfold sqrt_up.a:t
Ha:a <= 0
match compare 0 a with
| Lt => S √ (P a)
| _ => 0
end == 0 case compare_spec; try order.
Qed.

Lemma sqrt_up_eqn : forall a, 0<a -> √°a == S √(P a).forall a : t, 0 < a -> √° a == S √ (P a)
Proof.forall a : t, 0 < a -> √° a == S √ (P a)
 intros a Ha.a:t
Ha:0 < a
√° a == S √ (P a) unfold sqrt_up.a:t
Ha:0 < a
match compare 0 a with
| Lt => S √ (P a)
| _ => 0
end == S √ (P a) case compare_spec; try order.
Qed.

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

First, sqrt_up is non-negative

Lemma sqrt_up_nonneg : forall a, 0<=√°a.forall a : t, 0 <= √° a
Proof.forall a : t, 0 <= √° a
 intros.a:t
0 <= √° a destruct (le_gt_cases a 0) as [Ha|Ha].a:t
Ha:a <= 0
0 <= √° a
a:t
Ha:0 < a
0 <= √° a
 -a:t
Ha:a <= 0
0 <= √° a now rewrite sqrt_up_eqn0.
 -a:t
Ha:0 < a
0 <= √° a rewrite sqrt_up_eqn; trivial.a:t
Ha:0 < a
0 <= S √ (P a) apply le_le_succ_r, sqrt_nonneg.
Qed.

sqrt_up is a morphism

Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up.Proper (eq ==> eq) sqrt_up
Proof.Proper (eq ==> eq) sqrt_up
 assert (Proper (eq==>eq==>Logic.eq) compare).Proper (eq ==> eq ==> Logic.eq) compare
H:Proper (eq ==> eq ==> Logic.eq) compare
Proper (eq ==> eq) sqrt_up
 -Proper (eq ==> eq ==> Logic.eq) compare intros x x' Hx y y' Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
compare x y = compare x' y' do 2 case compare_spec; trivial; order.
 -H:Proper (eq ==> eq ==> Logic.eq) compare
Proper (eq ==> eq) sqrt_up intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx.
Qed.

The spec of sqrt_up indeed determines it

Lemma sqrt_up_unique : forall a b, 0<b -> (P b)² < a <= b² -> √°a == b.forall a b : t, 0 < b -> (P b)² < a <= b² -> √° a == b
Proof.forall a b : t, 0 < b -> (P b)² < a <= b² -> √° a == b
 intros a b Hb (LEb,LTb).a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
√° a == b
 assert (Ha : 0<a)
  by (apply le_lt_trans with (P b)²; trivial using square_nonneg).a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
√° a == b
 rewrite sqrt_up_eqn; trivial.a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
S √ (P a) == b
 assert (Hb' := lt_succ_pred 0 b Hb).a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
Hb':S (P b) == b
S √ (P a) == b
 rewrite <- Hb'.a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
Hb':S (P b) == b
S √ (P a) == S (P b) f_equiv.a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
Hb':S (P b) == b
√ (P a) == P b apply sqrt_unique.a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
Hb':S (P b) == b
(P b)² <= P a < (S (P b))²
 rewrite <- le_succ_l, <- lt_succ_r, Hb'.a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
Hb':S (P b) == b
(P b)² < S (P a) <= b²
 rewrite (lt_succ_pred 0 a Ha).a, b:t
Hb:0 < b
LEb:(P b)² < a
LTb:a <= b²
Ha:0 < a
Hb':S (P b) == b
(P b)² < a <= b² now split.
Qed.

sqrt_up is exact on squares

Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a.forall a : t, 0 <= a -> √° a² == a
Proof.forall a : t, 0 <= a -> √° a² == a
 intros a Ha.a:t
Ha:0 <= a
√° a² == a
 le_elim Ha.a:t
Ha:0 < a
√° a² == a
a:t
Ha:0 == a
√° a² == a
 -a:t
Ha:0 < a
√° a² == a rewrite sqrt_up_eqn by (now apply mul_pos_pos).a:t
Ha:0 < a
S √ (P a²) == a
   rewrite sqrt_pred_square; trivial.a:t
Ha:0 < a
S (P a) == a apply (lt_succ_pred 0); trivial.
 -a:t
Ha:0 == a
√° a² == a rewrite sqrt_up_eqn0; trivial.a:t
Ha:0 == a
a² <= 0 rewrite <- Ha.a:t
Ha:0 == a
0² <= 0 now nzsimpl.
Qed.

sqrt_up and successors of squares

Lemma sqrt_up_succ_square : forall a, 0<=a -> √°(S a²) == S a.forall a : t, 0 <= a -> √° (S a²) == S a
Proof.forall a : t, 0 <= a -> √° (S a²) == S a
 intros a Ha.a:t
Ha:0 <= a
√° (S a²) == S a
 rewrite sqrt_up_eqn by (now apply lt_succ_r, mul_nonneg_nonneg).a:t
Ha:0 <= a
S √ (P (S a²)) == S a
 now rewrite pred_succ, sqrt_square.
Qed.

Basic constants

Lemma sqrt_up_0 : √°0 == 0.√° 0 == 0
Proof.√° 0 == 0
 rewrite <- (mul_0_l 0) at 1.√° 0² == 0 now apply sqrt_up_square.
Qed.

Lemma sqrt_up_1 : √°1 == 1.√° 1 == 1
Proof.√° 1 == 1
 rewrite <- (mul_1_l 1) at 1.√° 1² == 1 apply sqrt_up_square.0 <= 1 order'.
Qed.

Lemma sqrt_up_2 : √°2 == 2.√° 2 == 2
Proof.√° 2 == 2
 rewrite sqrt_up_eqn by order'.S √ (P 2) == 2
 now rewrite two_succ, pred_succ, sqrt_1.
Qed.

Links between sqrt and sqrt_up

Lemma le_sqrt_sqrt_up : forall a, √a <= √°a.forall a : t, √ a <= √° a
Proof.forall a : t, √ a <= √° a
 intros a.a:t
√ a <= √° a unfold sqrt_up.a:t
√ a <=
match compare 0 a with
| Lt => S √ (P a)
| _ => 0
end case compare_spec; intros H.a:t
H:0 == a
√ a <= 0
a:t
H:0 < a
√ a <= S √ (P a)
a:t
H:a < 0
√ a <= 0
 -a:t
H:0 == a
√ a <= 0 rewrite <- H, sqrt_0.a:t
H:0 == a
0 <= 0 order.
 -a:t
H:0 < a
√ a <= S √ (P a) rewrite <- (lt_succ_pred 0 a H) at 1.a:t
H:0 < a
√ (S (P a)) <= S √ (P a) apply sqrt_succ_le.a:t
H:0 < a
0 <= P a
   apply lt_succ_r.a:t
H:0 < a
0 < S (P a) now rewrite (lt_succ_pred 0 a H).
 -a:t
H:a < 0
√ a <= 0 now rewrite sqrt_neg.
Qed.

Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a).forall a : t, √° a <= S √ a
Proof.forall a : t, √° a <= S √ a
 intros a.a:t
√° a <= S √ a unfold sqrt_up.a:t
match compare 0 a with
| Lt => S √ (P a)
| _ => 0
end <= S √ a
 case compare_spec; intros H; try apply le_le_succ_r, sqrt_nonneg.a:t
H:0 < a
S √ (P a) <= S √ a
 rewrite <- succ_le_mono.a:t
H:0 < a
√ (P a) <= √ a apply sqrt_le_mono.a:t
H:0 < a
P a <= a
 rewrite <- (lt_succ_pred 0 a H) at 2.a:t
H:0 < a
P a <= S (P a) apply le_succ_diag_r.
Qed.

Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)².forall a : t, 0 <= a -> (√ a)² <= a <= (√° a)²
Proof.forall a : t, 0 <= a -> (√ a)² <= a <= (√° a)²
 intros a H.a:t
H:0 <= a
(√ a)² <= a <= (√° a)² split.a:t
H:0 <= a
(√ a)² <= a
a:t
H:0 <= a
a <= (√° a)²
 -a:t
H:0 <= a
(√ a)² <= a now apply sqrt_spec.
 -a:t
H:0 <= a
a <= (√° a)² le_elim H.a:t
H:0 < a
a <= (√° a)²
a:t
H:0 == a
a <= (√° a)²
   +a:t
H:0 < a
a <= (√° a)² now apply sqrt_up_spec.
   +a:t
H:0 == a
a <= (√° a)² now rewrite <-H, sqrt_up_0, mul_0_l.
Qed.

Lemma sqrt_sqrt_up_exact :
 forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²).forall a : t,
0 <= a ->
√ a == √° a <-> (exists b : t, 0 <= b /\ a == b²)
Proof.forall a : t,
0 <= a ->
√ a == √° a <-> (exists b : t, 0 <= b /\ a == b²)
 intros a Ha.a:t
Ha:0 <= a
√ a == √° a <-> (exists b : t, 0 <= b /\ a == b²)
 split.a:t
Ha:0 <= a
√ a == √° a -> exists b : t, 0 <= b /\ a == b²
a:t
Ha:0 <= a
(exists b : t, 0 <= b /\ a == b²) -> √ a == √° a -a:t
Ha:0 <= a
√ a == √° a -> exists b : t, 0 <= b /\ a == b² intros.a:t
Ha:0 <= a
H:√ a == √° a
exists b : t, 0 <= b /\ a == b² exists √a.a:t
Ha:0 <= a
H:√ a == √° a
0 <= √ a /\ a == (√ a)²
          split.a:t
Ha:0 <= a
H:√ a == √° a
0 <= √ a
a:t
Ha:0 <= a
H:√ a == √° a
a == (√ a)² +a:t
Ha:0 <= a
H:√ a == √° a
0 <= √ a apply sqrt_nonneg.
          +a:t
Ha:0 <= a
H:√ a == √° a
a == (√ a)² generalize (sqrt_sqrt_up_spec a Ha).a:t
Ha:0 <= a
H:√ a == √° a
(√ a)² <= a <= (√° a)² -> a == (√ a)² rewrite <-H.a:t
Ha:0 <= a
H:√ a == √° a
(√ a)² <= a <= (√ a)² -> a == (√ a)² destruct 1; order.
 -a:t
Ha:0 <= a
(exists b : t, 0 <= b /\ a == b²) -> √ a == √° a intros (b & Hb & Hb').a:t
Ha:0 <= a
b:t
Hb:0 <= b
Hb':a == b²
√ a == √° a rewrite Hb'.a:t
Ha:0 <= a
b:t
Hb:0 <= b
Hb':a == b²
√ b² == √° b²
   now rewrite sqrt_square, sqrt_up_square.
Qed.

sqrt_up is a monotone function (but not a strict one)

Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b.forall a b : t, a <= b -> √° a <= √° b
Proof.forall a b : t, a <= b -> √° a <= √° b
 intros a b H.a, b:t
H:a <= b
√° a <= √° b
 destruct (le_gt_cases a 0) as [Ha|Ha].a, b:t
H:a <= b
Ha:a <= 0
√° a <= √° b
a, b:t
H:a <= b
Ha:0 < a
√° a <= √° b
 -a, b:t
H:a <= b
Ha:a <= 0
√° a <= √° b rewrite (sqrt_up_eqn0 _ Ha).a, b:t
H:a <= b
Ha:a <= 0
0 <= √° b apply sqrt_up_nonneg.
 -a, b:t
H:a <= b
Ha:0 < a
√° a <= √° b rewrite 2 sqrt_up_eqn by order.a, b:t
H:a <= b
Ha:0 < a
S √ (P a) <= S √ (P b) rewrite <- succ_le_mono.a, b:t
H:a <= b
Ha:0 < a
√ (P a) <= √ (P b)
   apply sqrt_le_mono, succ_le_mono.a, b:t
H:a <= b
Ha:0 < a
S (P a) <= S (P b) rewrite 2 (lt_succ_pred 0); order.
Qed.

No reverse result for <=, consider for instance √°3 <= √°2

Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b.forall a b : t, √° a < √° b -> a < b
Proof.forall a b : t, √° a < √° b -> a < b
 intros a b H.a, b:t
H:√° a < √° b
a < b
 destruct (le_gt_cases b 0) as [Hb|Hb].a, b:t
H:√° a < √° b
Hb:b <= 0
a < b
a, b:t
H:√° a < √° b
Hb:0 < b
a < b
 -a, b:t
H:√° a < √° b
Hb:b <= 0
a < b rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order.
 -a, b:t
H:√° a < √° b
Hb:0 < b
a < b destruct (le_gt_cases a 0) as [Ha|Ha]; [order|].a, b:t
H:√° a < √° b
Hb:0 < b
Ha:0 < a
a < b
   rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono.a, b:t
H:√° a < √° b
Hb:0 < b
Ha:0 < a
P a < P b
   apply sqrt_lt_cancel, succ_lt_mono.a, b:t
H:√° a < √° b
Hb:0 < b
Ha:0 < a
S √ (P a) < S √ (P b) now rewrite <- 2 sqrt_up_eqn.
Qed.

When left side is a square, we have an equivalence for <

Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a).forall a b : t,
0 <= a -> 0 <= b -> b² < a <-> b < √° a
Proof.forall a b : t,
0 <= a -> 0 <= b -> b² < a <-> b < √° a
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
b² < a <-> b < √° a split; intros H.a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
b < √° a
a, b:t
Ha:0 <= a
Hb:0 <= b
H:b < √° a
b² < a
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
b < √° a destruct (sqrt_up_spec a) as (LE,LT).a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
0 < a
a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
LE:(P √° a)² < a
LT:a <= (√° a)²
b < √° a
   +a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
0 < a apply le_lt_trans with b²; trivial using square_nonneg.
   +a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
LE:(P √° a)² < a
LT:a <= (√° a)²
b < √° a apply square_lt_simpl_nonneg; try order.a, b:t
Ha:0 <= a
Hb:0 <= b
H:b² < a
LE:(P √° a)² < a
LT:a <= (√° a)²
0 <= √° a apply sqrt_up_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:b < √° a
b² < a apply sqrt_up_lt_cancel.a, b:t
Ha:0 <= a
Hb:0 <= b
H:b < √° a
√° b² < √° a now rewrite sqrt_up_square.
Qed.

When right side is a square, we have an equivalence for <=

Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b).forall a b : t,
0 <= a -> 0 <= b -> a <= b² <-> √° a <= b
Proof.forall a b : t,
0 <= a -> 0 <= b -> a <= b² <-> √° a <= b
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
a <= b² <-> √° a <= b split; intros H.a, b:t
Ha:0 <= a
Hb:0 <= b
H:a <= b²
√° a <= b
a, b:t
Ha:0 <= a
Hb:0 <= b
H:√° a <= b
a <= b²
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:a <= b²
√° a <= b rewrite <- (sqrt_up_square b Hb).a, b:t
Ha:0 <= a
Hb:0 <= b
H:a <= b²
√° a <= √° b²
   now apply sqrt_up_le_mono.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
H:√° a <= b
a <= b² apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg].a, b:t
Ha:0 <= a
Hb:0 <= b
H:(√° a)² <= b²
a <= b²
   transitivity (√°a)²; trivial.a, b:t
Ha:0 <= a
Hb:0 <= b
H:(√° a)² <= b²
a <= (√° a)² now apply sqrt_sqrt_up_spec.
Qed.

Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a.forall a : t, 0 < √° a <-> 0 < a
Proof.forall a : t, 0 < √° a <-> 0 < a
  intros a.a:t
0 < √° a <-> 0 < a split; intros Ha.a:t
Ha:0 < √° a
0 < a
a:t
Ha:0 < a
0 < √° a -a:t
Ha:0 < √° a
0 < a apply sqrt_up_lt_cancel.a:t
Ha:0 < √° a
√° 0 < √° a now rewrite sqrt_up_0.
  -a:t
Ha:0 < a
0 < √° a rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1.a:t
Ha:0 < a
√° 1 <= √° a apply sqrt_up_le_mono.a:t
Ha:0 < a
1 <= a
    now rewrite one_succ, le_succ_l.
Qed.

Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a.forall a : t, 2 < a -> √° a < a
Proof.forall a : t, 2 < a -> √° a < a
 intros a Ha.a:t
Ha:2 < a
√° a < a
 rewrite sqrt_up_eqn by order'.a:t
Ha:2 < a
S √ (P a) < a
 assert (Ha' := lt_succ_pred 2 a Ha).a:t
Ha:2 < a
Ha':S (P a) == a
S √ (P a) < a
 rewrite <- Ha' at 2.a:t
Ha:2 < a
Ha':S (P a) == a
S √ (P a) < S (P a) rewrite <- succ_lt_mono.a:t
Ha:2 < a
Ha':S (P a) == a
√ (P a) < P a
 apply sqrt_lt_lin.a:t
Ha:2 < a
Ha':S (P a) == a
1 < P a rewrite succ_lt_mono.a:t
Ha:2 < a
Ha':S (P a) == a
S 1 < S (P a) now rewrite Ha', <- two_succ.
Qed.

Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a.forall a : t, 0 <= a -> √° a <= a
Proof.forall a : t, 0 <= a -> √° a <= a
 intros a Ha.a:t
Ha:0 <= a
√° a <= a
 le_elim Ha.a:t
Ha:0 < a
√° a <= a
a:t
Ha:0 == a
√° a <= a
 -a:t
Ha:0 < a
√° a <= a rewrite sqrt_up_eqn; trivial.a:t
Ha:0 < a
S √ (P a) <= a apply le_succ_l.a:t
Ha:0 < a
√ (P a) < a
   apply le_lt_trans with (P a).a:t
Ha:0 < a
√ (P a) <= P a
a:t
Ha:0 < a
P a < a +a:t
Ha:0 < a
√ (P a) <= P a apply sqrt_le_lin.a:t
Ha:0 < a
0 <= P a
                                   now rewrite <- lt_succ_r, (lt_succ_pred 0).
   +a:t
Ha:0 < a
P a < a rewrite <- (lt_succ_pred 0 a) at 2; trivial.a:t
Ha:0 < a
P a < S (P a) apply lt_succ_diag_r.
 -a:t
Ha:0 == a
√° a <= a now rewrite <- Ha, sqrt_up_0.
Qed.

sqrt_up and multiplication.

Due to rounding error, we don't have the usual √(a×b) = √a*√b but only lower and upper bounds.

Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √°b.forall a b : t,
0 <= a -> 0 <= b -> √° (a * b) <= √° a * √° b
Proof.forall a b : t,
0 <= a -> 0 <= b -> √° (a * b) <= √° a * √° b
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
√° (a * b) <= √° a * √° b
 apply sqrt_up_le_square.a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a * b
a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= √° a * √° b
a, b:t
Ha:0 <= a
Hb:0 <= b
a * b <= (√° a * √° b)²
 -a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= a * b now apply mul_nonneg_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
0 <= √° a * √° b apply mul_nonneg_nonneg; apply sqrt_up_nonneg.
 -a, b:t
Ha:0 <= a
Hb:0 <= b
a * b <= (√° a * √° b)² rewrite mul_shuffle1.a, b:t
Ha:0 <= a
Hb:0 <= b
a * b <= (√° a)² * (√° b)²
   apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec.
Qed.

Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b).forall a b : t,
0 < a -> 0 < b -> P √° a * P √° b < √° (a * b)
Proof.forall a b : t,
0 < a -> 0 < b -> P √° a * P √° b < √° (a * b)
 intros a b Ha Hb.a, b:t
Ha:0 < a
Hb:0 < b
P √° a * P √° b < √° (a * b)
 apply sqrt_up_lt_square.a, b:t
Ha:0 < a
Hb:0 < b
0 <= a * b
a, b:t
Ha:0 < a
Hb:0 < b
0 <= P √° a * P √° b
a, b:t
Ha:0 < a
Hb:0 < b
(P √° a * P √° b)² < a * b
 -a, b:t
Ha:0 < a
Hb:0 < b
0 <= a * b apply mul_nonneg_nonneg; order.
 -a, b:t
Ha:0 < a
Hb:0 < b
0 <= P √° a * P √° b apply mul_nonneg_nonneg; apply lt_succ_r.a, b:t
Ha:0 < a
Hb:0 < b
0 < S (P √° a)
a, b:t
Ha:0 < a
Hb:0 < b
0 < S (P √° b)
   +a, b:t
Ha:0 < a
Hb:0 < b
0 < S (P √° a) rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
   +a, b:t
Ha:0 < a
Hb:0 < b
0 < S (P √° b) rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
 -a, b:t
Ha:0 < a
Hb:0 < b
(P √° a * P √° b)² < a * b rewrite mul_shuffle1.a, b:t
Ha:0 < a
Hb:0 < b
(P √° a)² * (P √° b)² < a * b
   apply mul_lt_mono_nonneg; trivial using square_nonneg;
     now apply sqrt_up_spec.
Qed.

And we can't find better approximations in general.

The upper bound is exact for squares
Concerning the lower bound, for any c>0, take a=b=c²+1, then √°(a×b) = c²+1 while P √°a = P √°b = c

sqrt_up and successor :

the sqrt_up function climbs by at most 1 at a time
otherwise it stays at the same value
the +1 steps occur after squares

Lemma sqrt_up_succ_le : forall a, 0<=a -> √°(S a) <= S (√°a).forall a : t, 0 <= a -> √° (S a) <= S √° a
Proof.forall a : t, 0 <= a -> √° (S a) <= S √° a
 intros a Ha.a:t
Ha:0 <= a
√° (S a) <= S √° a
 apply sqrt_up_le_square.a:t
Ha:0 <= a
0 <= S a
a:t
Ha:0 <= a
0 <= S √° a
a:t
Ha:0 <= a
S a <= (S √° a)²
 -a:t
Ha:0 <= a
0 <= S a now apply le_le_succ_r.
 -a:t
Ha:0 <= a
0 <= S √° a apply le_le_succ_r, sqrt_up_nonneg.
 -a:t
Ha:0 <= a
S a <= (S √° a)² rewrite <- (add_1_l (√°a)).a:t
Ha:0 <= a
S a <= (1 + √° a)²
   apply le_trans with (1²+(√°a)²).a:t
Ha:0 <= a
S a <= 1² + (√° a)²
a:t
Ha:0 <= a
1² + (√° a)² <= (1 + √° a)²
   +a:t
Ha:0 <= a
S a <= 1² + (√° a)² rewrite mul_1_l, add_1_l, <- succ_le_mono.a:t
Ha:0 <= a
a <= (√° a)²
     now apply sqrt_sqrt_up_spec.
   +a:t
Ha:0 <= a
1² + (√° a)² <= (1 + √° a)² apply add_square_le.a:t
Ha:0 <= a
0 <= 1
a:t
Ha:0 <= a
0 <= √° a *a:t
Ha:0 <= a
0 <= 1 order'. *a:t
Ha:0 <= a
0 <= √° a apply sqrt_up_nonneg.
Qed.

Lemma sqrt_up_succ_or : forall a, 0<=a -> √°(S a) == S (√°a) \/ √°(S a) == √°a.forall a : t,
0 <= a -> √° (S a) == S √° a \/ √° (S a) == √° a
Proof.forall a : t,
0 <= a -> √° (S a) == S √° a \/ √° (S a) == √° a
 intros a Ha.a:t
Ha:0 <= a
√° (S a) == S √° a \/ √° (S a) == √° a
 destruct (le_gt_cases (√°(S a)) (√°a)) as [H|H].a:t
Ha:0 <= a
H:√° (S a) <= √° a
√° (S a) == S √° a \/ √° (S a) == √° a
a:t
Ha:0 <= a
H:√° a < √° (S a)
√° (S a) == S √° a \/ √° (S a) == √° a
 -a:t
Ha:0 <= a
H:√° (S a) <= √° a
√° (S a) == S √° a \/ √° (S a) == √° a right.a:t
Ha:0 <= a
H:√° (S a) <= √° a
√° (S a) == √° a generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order.
 -a:t
Ha:0 <= a
H:√° a < √° (S a)
√° (S a) == S √° a \/ √° (S a) == √° a left.a:t
Ha:0 <= a
H:√° a < √° (S a)
√° (S a) == S √° a apply le_succ_l in H.a:t
Ha:0 <= a
H:S √° a <= √° (S a)
√° (S a) == S √° a generalize (sqrt_up_succ_le a Ha); order.
Qed.

Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a ->
 (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²).forall a : t,
0 <= a ->
√° (S a) == S √° a <->
(exists b : t, 0 <= b /\ a == b²)
Proof.forall a : t,
0 <= a ->
√° (S a) == S √° a <->
(exists b : t, 0 <= b /\ a == b²)
 intros a Ha.a:t
Ha:0 <= a
√° (S a) == S √° a <->
(exists b : t, 0 <= b /\ a == b²) split.a:t
Ha:0 <= a
√° (S a) == S √° a -> exists b : t, 0 <= b /\ a == b²
a:t
Ha:0 <= a
(exists b : t, 0 <= b /\ a == b²) ->
√° (S a) == S √° a
 -a:t
Ha:0 <= a
√° (S a) == S √° a -> exists b : t, 0 <= b /\ a == b² intros EQ.a:t
Ha:0 <= a
EQ:√° (S a) == S √° a
exists b : t, 0 <= b /\ a == b²
   le_elim Ha.a:t
Ha:0 < a
EQ:√° (S a) == S √° a
exists b : t, 0 <= b /\ a == b²
a:t
Ha:0 == a
EQ:√° (S a) == S √° a
exists b : t, 0 <= b /\ a == b²
   +a:t
Ha:0 < a
EQ:√° (S a) == S √° a
exists b : t, 0 <= b /\ a == b² exists (√°a).a:t
Ha:0 < a
EQ:√° (S a) == S √° a
0 <= √° a /\ a == (√° a)² split.a:t
Ha:0 < a
EQ:√° (S a) == S √° a
0 <= √° a
a:t
Ha:0 < a
EQ:√° (S a) == S √° a
a == (√° a)² *a:t
Ha:0 < a
EQ:√° (S a) == S √° a
0 <= √° a apply sqrt_up_nonneg.
     *a:t
Ha:0 < a
EQ:√° (S a) == S √° a
a == (√° a)² generalize (proj2 (sqrt_up_spec a Ha)).a:t
Ha:0 < a
EQ:√° (S a) == S √° a
a <= (√° a)² -> a == (√° a)²
       assert (Ha' : 0 < S a) by (apply lt_succ_r; order').a:t
Ha:0 < a
EQ:√° (S a) == S √° a
Ha':0 < S a
a <= (√° a)² -> a == (√° a)²
       generalize (proj1 (sqrt_up_spec (S a) Ha')).a:t
Ha:0 < a
EQ:√° (S a) == S √° a
Ha':0 < S a
(P √° (S a))² < S a -> a <= (√° a)² -> a == (√° a)²
       rewrite EQ, pred_succ, lt_succ_r.a:t
Ha:0 < a
EQ:√° (S a) == S √° a
Ha':0 < S a
(√° a)² <= a -> a <= (√° a)² -> a == (√° a)² order.
   +a:t
Ha:0 == a
EQ:√° (S a) == S √° a
exists b : t, 0 <= b /\ a == b² exists 0.a:t
Ha:0 == a
EQ:√° (S a) == S √° a
0 <= 0 /\ a == 0² nzsimpl.a:t
Ha:0 == a
EQ:√° (S a) == S √° a
0 <= 0 /\ a == 0 now split.
 -a:t
Ha:0 <= a
(exists b : t, 0 <= b /\ a == b²) ->
√° (S a) == S √° a intros (b & Hb & H).a:t
Ha:0 <= a
b:t
Hb:0 <= b
H:a == b²
√° (S a) == S √° a
   now rewrite H, sqrt_up_succ_square, sqrt_up_square.
Qed.

sqrt_up and addition

Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b.forall a b : t, √° (a + b) <= √° a + √° b
Proof.forall a b : t, √° (a + b) <= √° a + √° b
 assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b).forall a b : t, a <= 0 -> √° (a + b) <= √° a + √° b
AUX:forall a b : t, a <= 0 -> √° (a + b) <= √° a + √° b
forall a b : t, √° (a + b) <= √° a + √° b
 -forall a b : t, a <= 0 -> √° (a + b) <= √° a + √° b intros a b Ha.a, b:t
Ha:a <= 0
√° (a + b) <= √° a + √° b rewrite (sqrt_up_eqn0 a Ha).a, b:t
Ha:a <= 0
√° (a + b) <= 0 + √° b nzsimpl.a, b:t
Ha:a <= 0
√° (a + b) <= √° b
   apply sqrt_up_le_mono.a, b:t
Ha:a <= 0
a + b <= b
   rewrite <- (add_0_l b) at 2.a, b:t
Ha:a <= 0
a + b <= 0 + b
   apply add_le_mono_r; order.
 -AUX:forall a b : t, a <= 0 -> √° (a + b) <= √° a + √° b
forall a b : t, √° (a + b) <= √° a + √° b intros a b.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
√° (a + b) <= √° a + √° b
   destruct (le_gt_cases a 0) as [Ha|Ha].AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:a <= 0
√° (a + b) <= √° a + √° b
AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
√° (a + b) <= √° a + √° b +AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:a <= 0
√° (a + b) <= √° a + √° b now apply AUX.
   +AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
√° (a + b) <= √° a + √° b destruct (le_gt_cases b 0) as [Hb|Hb].AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:b <= 0
√° (a + b) <= √° a + √° b
AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√° (a + b) <= √° a + √° b
     *AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:b <= 0
√° (a + b) <= √° a + √° b rewrite (add_comm a), (add_comm (√°a)); now apply AUX.
     *AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√° (a + b) <= √° a + √° b rewrite 2 sqrt_up_eqn; trivial.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
S √ (P (a + b)) <= S √ (P a) + √° b
AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
0 < a + b
       --AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
S √ (P (a + b)) <= S √ (P a) + √° b nzsimpl.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
S √ (P (a + b)) <= S (√ (P a) + √° b) rewrite <- succ_le_mono.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P (a + b)) <= √ (P a) + √° b
          transitivity (√(P a) + √b).AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P (a + b)) <= √ (P a) + √ b
AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P a) + √ b <= √ (P a) + √° b
          ++AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P (a + b)) <= √ (P a) + √ b rewrite <- (lt_succ_pred 0 a Ha) at 1.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P (S (P a) + b)) <= √ (P a) + √ b nzsimpl.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P a + b) <= √ (P a) + √ b apply sqrt_add_le.
          ++AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ (P a) + √ b <= √ (P a) + √° b apply add_le_mono_l.AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
√ b <= √° b
             apply le_sqrt_sqrt_up.
       --AUX:forall a0 b0 : t, a0 <= 0 -> √° (a0 + b0) <= √° a0 + √° b0
a, b:t
Ha:0 < a
Hb:0 < b
0 < a + b now apply add_pos_pos.
Qed.

Convexity-like inequality for sqrt_up: sqrt_up of middle is above middle of square roots. We cannot say more, for instance take a=b=2, then 2+2 <= S 3

Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)).forall a b : t,
0 <= a -> 0 <= b -> √° a + √° b <= S √° (2 * (a + b))
Proof.forall a b : t,
0 <= a -> 0 <= b -> √° a + √° b <= S √° (2 * (a + b))
 intros a b Ha Hb.a, b:t
Ha:0 <= a
Hb:0 <= b
√° a + √° b <= S √° (2 * (a + b))
 le_elim Ha;[le_elim Hb|].a, b:t
Ha:0 < a
Hb:0 < b
√° a + √° b <= S √° (2 * (a + b))
a, b:t
Ha:0 < a
Hb:0 == b
√° a + √° b <= S √° (2 * (a + b))
a, b:t
Ha:0 == a
Hb:0 <= b
√° a + √° b <= S √° (2 * (a + b))
 -a, b:t
Ha:0 < a
Hb:0 < b
√° a + √° b <= S √° (2 * (a + b)) rewrite 3 sqrt_up_eqn; trivial.a, b:t
Ha:0 < a
Hb:0 < b
S √ (P a) + S √ (P b) <= S (S √ (P (2 * (a + b))))
a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 * (a + b)
   +a, b:t
Ha:0 < a
Hb:0 < b
S √ (P a) + S √ (P b) <= S (S √ (P (2 * (a + b)))) nzsimpl.a, b:t
Ha:0 < a
Hb:0 < b
S (S (√ (P a) + √ (P b))) <= S (S √ (P (2 * (a + b)))) rewrite <- 2 succ_le_mono.a, b:t
Ha:0 < a
Hb:0 < b
√ (P a) + √ (P b) <= √ (P (2 * (a + b)))
     etransitivity; [eapply add_sqrt_le|].a, b:t
Ha:0 < a
Hb:0 < b
0 <= P a
a, b:t
Ha:0 < a
Hb:0 < b
0 <= P b
a, b:t
Ha:0 < a
Hb:0 < b
√ (2 * (P a + P b)) <= √ (P (2 * (a + b)))
     *a, b:t
Ha:0 < a
Hb:0 < b
0 <= P a apply lt_succ_r.a, b:t
Ha:0 < a
Hb:0 < b
0 < S (P a) now rewrite (lt_succ_pred 0 a Ha).
     *a, b:t
Ha:0 < a
Hb:0 < b
0 <= P b apply lt_succ_r.a, b:t
Ha:0 < a
Hb:0 < b
0 < S (P b) now rewrite (lt_succ_pred 0 b Hb).
     *a, b:t
Ha:0 < a
Hb:0 < b
√ (2 * (P a + P b)) <= √ (P (2 * (a + b))) apply sqrt_le_mono.a, b:t
Ha:0 < a
Hb:0 < b
2 * (P a + P b) <= P (2 * (a + b))
       apply lt_succ_r.a, b:t
Ha:0 < a
Hb:0 < b
2 * (P a + P b) < S (P (2 * (a + b))) rewrite (lt_succ_pred 0).a, b:t
Ha:0 < a
Hb:0 < b
2 * (P a + P b) < 2 * (a + b)
a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 * (a + b)
       --a, b:t
Ha:0 < a
Hb:0 < b
2 * (P a + P b) < 2 * (a + b) apply mul_lt_mono_pos_l.a, b:t
Ha:0 < a
Hb:0 < b
0 < 2
a, b:t
Ha:0 < a
Hb:0 < b
P a + P b < a + b ++a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 order'.
          ++a, b:t
Ha:0 < a
Hb:0 < b
P a + P b < a + b apply add_lt_mono.a, b:t
Ha:0 < a
Hb:0 < b
P a < a
a, b:t
Ha:0 < a
Hb:0 < b
P b < b
             **a, b:t
Ha:0 < a
Hb:0 < b
P a < a apply le_succ_l.a, b:t
Ha:0 < a
Hb:0 < b
S (P a) <= a now rewrite (lt_succ_pred 0).
             **a, b:t
Ha:0 < a
Hb:0 < b
P b < b apply le_succ_l.a, b:t
Ha:0 < a
Hb:0 < b
S (P b) <= b now rewrite (lt_succ_pred 0).
       --a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 * (a + b) apply mul_pos_pos.a, b:t
Ha:0 < a
Hb:0 < b
0 < 2
a, b:t
Ha:0 < a
Hb:0 < b
0 < a + b ++a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 order'. ++a, b:t
Ha:0 < a
Hb:0 < b
0 < a + b now apply add_pos_pos.
   +a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 * (a + b) apply mul_pos_pos.a, b:t
Ha:0 < a
Hb:0 < b
0 < 2
a, b:t
Ha:0 < a
Hb:0 < b
0 < a + b *a, b:t
Ha:0 < a
Hb:0 < b
0 < 2 order'. *a, b:t
Ha:0 < a
Hb:0 < b
0 < a + b now apply add_pos_pos.
 -a, b:t
Ha:0 < a
Hb:0 == b
√° a + √° b <= S √° (2 * (a + b)) rewrite <- Hb, sqrt_up_0.a, b:t
Ha:0 < a
Hb:0 == b
√° a + 0 <= S √° (2 * (a + 0)) nzsimpl.a, b:t
Ha:0 < a
Hb:0 == b
√° a <= S √° (2 * a) apply le_le_succ_r, sqrt_up_le_mono.a, b:t
Ha:0 < a
Hb:0 == b
a <= 2 * a
   rewrite <- (mul_1_l a) at 1.a, b:t
Ha:0 < a
Hb:0 == b
1 * a <= 2 * a apply mul_le_mono_nonneg_r; order'.
 -a, b:t
Ha:0 == a
Hb:0 <= b
√° a + √° b <= S √° (2 * (a + b)) rewrite <- Ha, sqrt_up_0.a, b:t
Ha:0 == a
Hb:0 <= b
0 + √° b <= S √° (2 * (0 + b)) nzsimpl.a, b:t
Ha:0 == a
Hb:0 <= b
√° b <= S √° (2 * b) apply le_le_succ_r, sqrt_up_le_mono.a, b:t
Ha:0 == a
Hb:0 <= b
b <= 2 * b
   rewrite <- (mul_1_l b) at 1.a, b:t
Ha:0 == a
Hb:0 <= b
1 * b <= 2 * b apply mul_le_mono_nonneg_r; order'.
Qed.

End NZSqrtUpProp.