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.

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Helper functions and theorems for computing the rounded square root of a floating-point number.

Require Import Raux Defs Digits Generic_fmt Float_prop Bracket.

Set Implicit Arguments.
Set Strongly Strict Implicit.

Section Fcalc_sqrt.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.

Computes a mantissa of precision p, the corresponding exponent, and the position with respect to the real square root of the input floating-point number.

The algorithm performs the following steps:

Shift the mantissa so that it has at least 2p-1 digits; shift it one digit more if the new exponent is not even.
Compute the square root s (at least p digits) of the new mantissa, and its remainder r.
Compute the position according to the remainder:
- - r == 0 => Eq,
- - r <= s => Lo,
- - r >= s => Up.

Complexity is fine as long as p1 <= 2p-1.

Lemma mag_sqrt_F2R :
  forall m1 e1,
  (0 < m1)%Z ->
  mag beta (sqrt (F2R (Float beta m1 e1))) = Z.div2 (Zdigits beta m1 + e1 + 1) :> Z.beta:radix
fexp:Z -> Z
forall m1 e1 : Z,
(0 < m1)%Z ->
mag beta (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) =
Z.div2 (Zdigits beta m1 + e1 + 1)
Proof.beta:radix
fexp:Z -> Z
forall m1 e1 : Z,
(0 < m1)%Z ->
mag beta (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) =
Z.div2 (Zdigits beta m1 + e1 + 1)
intros m1 e1 Hm1.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
mag beta (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) =
Z.div2 (Zdigits beta m1 + e1 + 1)
rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
mag beta (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) =
Z.div2
  (mag beta (F2R {| Fnum := m1; Fexp := e1 |}) + 1)
apply mag_sqrt.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
(0 < F2R {| Fnum := m1; Fexp := e1 |})%R
now apply F2R_gt_0.
Qed.

Definition Fsqrt_core m1 e1 e :=
  let d1 := Zdigits beta m1 in
  let m1' := (m1 * Zpower beta (e1 - 2 * e))%Z in
  let (q, r) := Z.sqrtrem m1' in
  let l :=
    if Zeq_bool r 0 then loc_Exact
    else loc_Inexact (if Zle_bool r q then Lt else Gt) in
  (q, l).

Theorem Fsqrt_core_correct :
  forall m1 e1 e,
  (0 < m1)%Z ->
  (2 * e <= e1)%Z ->
  let '(m, l) := Fsqrt_core m1 e1 e in
  inbetween_float beta m e (sqrt (F2R (Float beta m1 e1))) l.beta:radix
fexp:Z -> Z
forall m1 e1 e : Z,
(0 < m1)%Z ->
(2 * e <= e1)%Z ->
let
'(m, l) := Fsqrt_core m1 e1 e in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
Proof.beta:radix
fexp:Z -> Z
forall m1 e1 e : Z,
(0 < m1)%Z ->
(2 * e <= e1)%Z ->
let
'(m, l) := Fsqrt_core m1 e1 e in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
intros m1 e1 e Hm1 He.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
let
'(m, l) := Fsqrt_core m1 e1 e in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
unfold Fsqrt_core.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
let
'(m, l) :=
 let (q, r) := Z.sqrtrem (m1 * beta ^ (e1 - 2 * e)) in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
set (m' := Zmult _ _).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
let
'(m, l) :=
 let (q, r) := Z.sqrtrem m' in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
assert (0 <= m')%Z as Hm'.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
(0 <= m')%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
let
'(m, l) :=
 let (q, r) := Z.sqrtrem m' in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
{beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
(0 <= m')%Z apply Z.mul_nonneg_nonneg.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
(0 <= m1)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
(0 <= beta ^ (e1 - 2 * e))%Z
  now apply Zlt_le_weak.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
(0 <= beta ^ (e1 - 2 * e))%Z
  apply Zpower_ge_0. }beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
let
'(m, l) :=
 let (q, r) := Z.sqrtrem m' in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
assert (sqrt (F2R (Float beta m1 e1)) = sqrt (IZR m') * bpow e)%R as Hf.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
let
'(m, l) :=
 let (q, r) := Z.sqrtrem m' in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
{beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R rewrite <- (sqrt_Rsqr (bpow e)) by apply bpow_ge_0.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * sqrt (bpow e)²)%R
  rewrite <- sqrt_mult.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
sqrt (IZR m' * (bpow e)²)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= (bpow e)²)%R
  unfold Rsqr, m'.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
sqrt
  (IZR (m1 * beta ^ (e1 - 2 * e)) * (bpow e * bpow e))
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= (bpow e)²)%R
  rewrite mult_IZR, IZR_Zpower by omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
sqrt (IZR m1 * bpow (e1 - 2 * e) * (bpow e * bpow e))
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= (bpow e)²)%R
  rewrite Rmult_assoc, <- 2!bpow_plus.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
sqrt (IZR m1 * bpow (e1 - 2 * e + (e + e)))
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= (bpow e)²)%R
  now replace (_ + _)%Z with e1 by ring.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= (bpow e)²)%R
  now apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
(0 <= (bpow e)²)%R
  apply Rle_0_sqr. }beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
let
'(m, l) :=
 let (q, r) := Z.sqrtrem m' in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
generalize (Z.sqrtrem_spec m' Hm').beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
(let (s, r) := Z.sqrtrem m' in
 m' = (s * s + r)%Z /\ (0 <= r <= 2 * s)%Z) ->
let
'(m, l) :=
 let (q, r) := Z.sqrtrem m' in
 (q,
 if Zeq_bool r 0
 then SpecFloatCopy.loc_Exact
 else
  SpecFloatCopy.loc_Inexact
    (if (r <=? q)%Z then Lt else Gt)) in
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
destruct Z.sqrtrem as [q r].beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
m' = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z ->
inbetween_float beta q e
  (sqrt (F2R {| Fnum := m1; Fexp := e1 |}))
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
intros [Hq Hr].beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween_float beta q e
  (sqrt (F2R {| Fnum := m1; Fexp := e1 |}))
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
rewrite Hf.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween_float beta q e (sqrt (IZR m') * bpow e)
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
unfold inbetween_float, F2R.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween
  (IZR (Fnum {| Fnum := q; Fexp := e |}) *
   bpow (Fexp {| Fnum := q; Fexp := e |}))
  (IZR (Fnum {| Fnum := q + 1; Fexp := e |}) *
   bpow (Fexp {| Fnum := q + 1; Fexp := e |}))
  (sqrt (IZR m') * bpow e)
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt)) simpl Fnum.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween
  (IZR q * bpow (Fexp {| Fnum := q; Fexp := e |}))
  (IZR (q + 1) *
   bpow (Fexp {| Fnum := q + 1; Fexp := e |}))
  (sqrt (IZR m') * bpow e)
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
apply inbetween_mult_compat.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
(0 < bpow e)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween (IZR q) (IZR (q + 1)) 
  (sqrt (IZR m'))
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
apply bpow_gt_0.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween (IZR q) (IZR (q + 1)) (sqrt (IZR m'))
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
rewrite Hq.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (if Zeq_bool r 0
   then SpecFloatCopy.loc_Exact
   else
    SpecFloatCopy.loc_Inexact
      (if (r <=? q)%Z then Lt else Gt))
case Zeq_bool_spec ; intros Hr'.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r))) SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
(* .. r = 0 *)
rewrite Hr', Zplus_0_r, mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
inbetween (IZR q) (IZR (q + 1)) (sqrt (IZR q * IZR q))
  SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
fold (Rsqr (IZR q)).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
inbetween (IZR q) (IZR (q + 1)) (sqrt (IZR q)²)
  SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
rewrite sqrt_Rsqr.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
inbetween (IZR q) (IZR (q + 1)) (IZR q)
  SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
(0 <= IZR q)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
now constructor.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
(0 <= IZR q)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r = 0%Z
(0 <= q)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
clear -Hr ; omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
inbetween (IZR q) (IZR (q + 1))
  (sqrt (IZR (q * q + r)))
  (SpecFloatCopy.loc_Inexact
     (if (r <=? q)%Z then Lt else Gt))
(* .. r <> 0 *)
constructor.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR q < sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
split.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR q < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
(* ... bounds *)
apply Rle_lt_trans with (sqrt (IZR (q * q))).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR q <= sqrt (IZR (q * q)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR q <= sqrt (IZR q * IZR q))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
fold (Rsqr (IZR q)).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR q <= sqrt (IZR q)²)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite sqrt_Rsqr.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR q <= IZR q)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply Rle_refl.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= q)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
clear -Hr ; omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q)) < sqrt (IZR (q * q + r)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply sqrt_lt_1.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q) < IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q * IZR q)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q) < IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply Rle_0_sqr.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q) < IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite <- Hq.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q) < IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
now apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q) < IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply IZR_lt.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(q * q < q * q + r)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) < IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply Rlt_le_trans with (sqrt (IZR ((q + 1) * (q + 1)))).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q * q + r)) <
 sqrt (IZR ((q + 1) * (q + 1))))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply sqrt_lt_1.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q + r) < IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite <- Hq.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q + r) < IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
now apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q + r) < IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q + 1) * IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q + r) < IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply Rle_0_sqr.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q * q + r) < IZR ((q + 1) * (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply IZR_lt.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(q * q + r < (q + 1) * (q + 1))%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
ring_simplify.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(q ^ 2 + r < q ^ 2 + 2 * q + 1)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR ((q + 1) * (q + 1))) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q + 1) * IZR (q + 1)) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
fold (Rsqr (IZR (q + 1))).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(sqrt (IZR (q + 1))² <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
rewrite sqrt_Rsqr.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(IZR (q + 1) <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply Rle_refl.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= q + 1)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
clear -Hr ; omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (sqrt (IZR (q * q + r)))
  ((IZR q + IZR (q + 1)) / 2) =
(if (r <=? q)%Z then Lt else Gt)
(* ... location *)
rewrite Rcompare_half_r.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (2 * sqrt (IZR (q * q + r)))
  (IZR q + IZR (q + 1)) =
(if (r <=? q)%Z then Lt else Gt)
generalize (Rcompare_sqr (2 * sqrt (IZR (q * q + r))) (IZR q + IZR (q + 1))).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare
  (2 * sqrt (IZR (q * q + r)) *
   (2 * sqrt (IZR (q * q + r))))
  ((IZR q + IZR (q + 1)) * (IZR q + IZR (q + 1))) =
Rcompare (Rabs (2 * sqrt (IZR (q * q + r))))
  (Rabs (IZR q + IZR (q + 1))) ->
Rcompare (2 * sqrt (IZR (q * q + r)))
  (IZR q + IZR (q + 1)) =
(if (r <=? q)%Z then Lt else Gt)
rewrite 2!Rabs_pos_eq.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare
  (2 * sqrt (IZR (q * q + r)) *
   (2 * sqrt (IZR (q * q + r))))
  ((IZR q + IZR (q + 1)) * (IZR q + IZR (q + 1))) =
Rcompare (2 * sqrt (IZR (q * q + r)))
  (IZR q + IZR (q + 1)) ->
Rcompare (2 * sqrt (IZR (q * q + r)))
  (IZR q + IZR (q + 1)) =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
intros <-.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare
  (2 * sqrt (IZR (q * q + r)) *
   (2 * sqrt (IZR (q * q + r))))
  ((IZR q + IZR (q + 1)) * (IZR q + IZR (q + 1))) =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
replace ((2 * sqrt (IZR (q * q + r))) * (2 * sqrt (IZR (q * q + r))))%R
  with (4 * Rsqr (sqrt (IZR (q * q + r))))%R by (unfold Rsqr ; ring).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (4 * (sqrt (IZR (q * q + r)))²)
  ((IZR q + IZR (q + 1)) * (IZR q + IZR (q + 1))) =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
rewrite Rsqr_sqrt.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (4 * IZR (q * q + r))
  ((IZR q + IZR (q + 1)) * (IZR q + IZR (q + 1))) =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
rewrite <- plus_IZR, <- 2!mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Rcompare (IZR (4 * (q * q + r)))
  (IZR ((q + (q + 1)) * (q + (q + 1)))) =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
rewrite Rcompare_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(4 * (q * q + r) ?= (q + (q + 1)) * (q + (q + 1)))%Z =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ring.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(4 * (q * q + r) ?= 4 * (q * q) + 4 * q + 1)%Z =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
generalize (Zle_cases r q).beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(if (r <=? q)%Z then (r <= q)%Z else (r > q)%Z) ->
(4 * (q * q + r) ?= 4 * (q * q) + 4 * q + 1)%Z =
(if (r <=? q)%Z then Lt else Gt)
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
case (Zle_bool r q) ; intros Hr''.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Hr'':(r <= q)%Z
(4 * (q * q + r) ?= 4 * (q * q) + 4 * q + 1)%Z = Lt
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Hr'':(r > q)%Z
(4 * (q * q + r) ?= 4 * (q * q) + 4 * q + 1)%Z = Gt
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
change (4 * (q * q + r) < 4 * (q * q) + 4 * q + 1)%Z.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Hr'':(r <= q)%Z
(4 * (q * q + r) < 4 * (q * q) + 4 * q + 1)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Hr'':(r > q)%Z
(4 * (q * q + r) ?= 4 * (q * q) + 4 * q + 1)%Z = Gt
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Hr'':(r > q)%Z
(4 * (q * q + r) ?= 4 * (q * q) + 4 * q + 1)%Z = Gt
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
change (4 * (q * q + r) > 4 * (q * q) + 4 * q + 1)%Z.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
Hr'':(r > q)%Z
(4 * (q * q + r) > 4 * (q * q) + 4 * q + 1)%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q * q + r))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
rewrite <- Hq.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR m')%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
now apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR q + IZR (q + 1))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
rewrite <- plus_IZR.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= IZR (q + (q + 1)))%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= q + (q + 1))%Z
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
clear -Hr ; omega.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2 * sqrt (IZR (q * q + r)))%R
apply Rmult_le_pos.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= 2)%R
beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= sqrt (IZR (q * q + r)))%R
now apply IZR_le.beta:radix
fexp:Z -> Z
m1, e1, e:Z
Hm1:(0 < m1)%Z
He:(2 * e <= e1)%Z
m':=(m1 * beta ^ (e1 - 2 * e))%Z:Z
Hm':(0 <= m')%Z
Hf:sqrt (F2R {| Fnum := m1; Fexp := e1 |}) =
(sqrt (IZR m') * bpow e)%R
q, r:Z
Hq:m' = (q * q + r)%Z
Hr:(0 <= r <= 2 * q)%Z
Hr':r <> 0%Z
(0 <= sqrt (IZR (q * q + r)))%R
apply sqrt_ge_0.
Qed.

Definition Fsqrt (x : float beta) :=
  let (m1, e1) := x in
  let e' := (Zdigits beta m1 + e1 + 1)%Z in
  let e := Z.min (fexp (Z.div2 e')) (Z.div2 e1) in
  let '(m, l) := Fsqrt_core m1 e1 e in
  (m, e, l).

Theorem Fsqrt_correct :
  forall x,
  (0 < F2R x)%R ->
  let '(m, e, l) := Fsqrt x in
  (e <= cexp beta fexp (sqrt (F2R x)))%Z /\
  inbetween_float beta m e (sqrt (F2R x)) l.beta:radix
fexp:Z -> Z
forall x : float beta,
(0 < F2R x)%R ->
let
'(m, e, l) := Fsqrt x in
 (e <= cexp beta fexp (sqrt (F2R x)))%Z /\
 inbetween_float beta m e (sqrt (F2R x)) l
Proof.beta:radix
fexp:Z -> Z
forall x : float beta,
(0 < F2R x)%R ->
let
'(m, e, l) := Fsqrt x in
 (e <= cexp beta fexp (sqrt (F2R x)))%Z /\
 inbetween_float beta m e (sqrt (F2R x)) l
intros [m1 e1] Hm1.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < F2R {| Fnum := m1; Fexp := e1 |})%R
let
'(m, e, l) := Fsqrt {| Fnum := m1; Fexp := e1 |} in
 (e <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
apply gt_0_F2R in Hm1.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
let
'(m, e, l) := Fsqrt {| Fnum := m1; Fexp := e1 |} in
 (e <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
unfold Fsqrt.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
let
'(m, e, l) :=
 let
 '(m, l) :=
  Fsqrt_core m1 e1
    (Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
       (Z.div2 e1)) in
  (m,
  Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
    (Z.div2 e1), l) in
 (e <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
set (e := Z.min _ _).beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
let
'(m, e0, l) :=
 let '(m, l) := Fsqrt_core m1 e1 e in (m, e, l) in
 (e0 <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e0
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
assert (2 * e <= e1)%Z as He.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
(2 * e <= e1)%Z
beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
let
'(m, e0, l) :=
 let '(m, l) := Fsqrt_core m1 e1 e in (m, e, l) in
 (e0 <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e0
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
{beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
(2 * e <= e1)%Z assert (e <= Z.div2 e1)%Z by apply Z.le_min_r.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
H:(e <= Z.div2 e1)%Z
(2 * e <= e1)%Z
  rewrite (Zdiv2_odd_eqn e1).beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
H:(e <= Z.div2 e1)%Z
(2 * e <= 2 * Z.div2 e1 + (if Z.odd e1 then 1 else 0))%Z
  destruct Z.odd ; omega. }beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
let
'(m, e0, l) :=
 let '(m, l) := Fsqrt_core m1 e1 e in (m, e, l) in
 (e0 <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e0
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
generalize (Fsqrt_core_correct m1 e1 e Hm1 He).beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
(let
 '(m, l) := Fsqrt_core m1 e1 e in
  inbetween_float beta m e
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l) ->
let
'(m, e0, l) :=
 let '(m, l) := Fsqrt_core m1 e1 e in (m, e, l) in
 (e0 <=
  cexp beta fexp
    (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
 inbetween_float beta m e0
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
destruct Fsqrt_core as [m l].beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
m:Z
l:SpecFloatCopy.location
inbetween_float beta m e
  (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l ->
(e <=
 cexp beta fexp
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z /\
inbetween_float beta m e
  (sqrt (F2R {| Fnum := m1; Fexp := e1 |})) l
apply conj.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
m:Z
l:SpecFloatCopy.location
(e <=
 cexp beta fexp
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z
apply Z.le_trans with (1 := Z.le_min_l _ _).beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
m:Z
l:SpecFloatCopy.location
(fexp (Z.div2 (Zdigits beta m1 + e1 + 1)) <=
 cexp beta fexp
   (sqrt (F2R {| Fnum := m1; Fexp := e1 |})))%Z
unfold cexp.beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
m:Z
l:SpecFloatCopy.location
(fexp (Z.div2 (Zdigits beta m1 + e1 + 1)) <=
 fexp
   (mag beta (sqrt (F2R {| Fnum := m1; Fexp := e1 |}))))%Z
rewrite (mag_sqrt_F2R m1 e1 Hm1).beta:radix
fexp:Z -> Z
m1, e1:Z
Hm1:(0 < m1)%Z
e:=Z.min (fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))
  (Z.div2 e1):Z
He:(2 * e <= e1)%Z
m:Z
l:SpecFloatCopy.location
(fexp (Z.div2 (Zdigits beta m1 + e1 + 1)) <=
 fexp (Z.div2 (Zdigits beta m1 + e1 + 1)))%Z
apply Z.le_refl.
Qed.

End Fcalc_sqrt.