Zaux.v

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.

From Coq Require Import ZArith Lia Zquot.

Require Import SpecFloatCompat.

Notation cond_Zopp := cond_Zopp (only parsing).
Notation iter_pos := iter_pos (only parsing).

Section Zmissing.

About Z

Theorem Zopp_le_cancel :
  forall x y : Z,
  (-y <= -x)%Z -> Z.le x y.forall x y : Z, (- y <= - x)%Z -> (x <= y)%Z
Proof.forall x y : Z, (- y <= - x)%Z -> (x <= y)%Z
intros x y Hxy.x, y:Z
Hxy:(- y <= - x)%Z
(x <= y)%Z
apply Zplus_le_reg_r with (-x - y)%Z.x, y:Z
Hxy:(- y <= - x)%Z
(x + (- x - y) <= y + (- x - y))%Z
now ring_simplify.
Qed.

Theorem Zgt_not_eq :
  forall x y : Z,
  (y < x)%Z -> (x <> y)%Z.forall x y : Z, (y < x)%Z -> x <> y
Proof.forall x y : Z, (y < x)%Z -> x <> y
intros x y H Hn.x, y:Z
H:(y < x)%Z
Hn:x = y
False
apply Z.lt_irrefl with x.x, y:Z
H:(y < x)%Z
Hn:x = y
(x < x)%Z
now rewrite Hn at 1.
Qed.

End Zmissing.

Section Proof_Irrelevance.

Scheme eq_dep_elim := Induction for eq Sort Type.

Definition eqbool_dep P (h1 : P true) b :=
  match b return P b -> Prop with
  | true => fun (h2 : P true) => h1 = h2
  | false => fun (h2 : P false) => False
  end.

Lemma eqbool_irrelevance : forall (b : bool) (h1 h2 : b = true), h1 = h2.forall (b : bool) (h1 h2 : b = true), h1 = h2
Proof.forall (b : bool) (h1 h2 : b = true), h1 = h2
assert (forall (h : true = true), refl_equal true = h).forall h : true = true, eq_refl = h
H:forall h : true = true, eq_refl = h
forall (b : bool) (h1 h2 : b = true), h1 = h2
apply (eq_dep_elim bool true (eqbool_dep _ _) (refl_equal _)).H:forall h : true = true, eq_refl = h
forall (b : bool) (h1 h2 : b = true), h1 = h2
intros b.H:forall h : true = true, eq_refl = h
b:bool
forall h1 h2 : b = true, h1 = h2
case b.H:forall h : true = true, eq_refl = h
b:bool
forall h1 h2 : true = true, h1 = h2
H:forall h : true = true, eq_refl = h
b:bool
forall h1 h2 : false = true, h1 = h2
intros h1 h2.H:forall h : true = true, eq_refl = h
b:bool
h1, h2:true = true
h1 = h2
H:forall h : true = true, eq_refl = h
b:bool
forall h1 h2 : false = true, h1 = h2
now rewrite <- (H h1).H:forall h : true = true, eq_refl = h
b:bool
forall h1 h2 : false = true, h1 = h2
intros h.H:forall h0 : true = true, eq_refl = h0
b:bool
h:false = true
forall h2 : false = true, h = h2
discriminate h.
Qed.

End Proof_Irrelevance.

Section Even_Odd.

Theorem Zeven_ex :
  forall x, exists p, x = (2 * p + if Z.even x then 0 else 1)%Z.forall x : Z,
exists p : Z,
  x = (2 * p + (if Z.even x then 0 else 1))%Z
Proof.forall x : Z,
exists p : Z,
  x = (2 * p + (if Z.even x then 0 else 1))%Z
intros [|[n|n|]|[n|n|]].exists p : Z,
  0%Z = (2 * p + (if Z.even 0 then 0 else 1))%Z
n:positive
exists p : Z,
  Z.pos n~1 =
  (2 * p + (if Z.even (Z.pos n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.pos n~0 =
  (2 * p + (if Z.even (Z.pos n~0) then 0 else 1))%Z
exists p : Z,
  1%Z = (2 * p + (if Z.even 1 then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~1 =
  (2 * p + (if Z.even (Z.neg n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
now exists Z0.n:positive
exists p : Z,
  Z.pos n~1 =
  (2 * p + (if Z.even (Z.pos n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.pos n~0 =
  (2 * p + (if Z.even (Z.pos n~0) then 0 else 1))%Z
exists p : Z,
  1%Z = (2 * p + (if Z.even 1 then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~1 =
  (2 * p + (if Z.even (Z.neg n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
now exists (Zpos n).n:positive
exists p : Z,
  Z.pos n~0 =
  (2 * p + (if Z.even (Z.pos n~0) then 0 else 1))%Z
exists p : Z,
  1%Z = (2 * p + (if Z.even 1 then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~1 =
  (2 * p + (if Z.even (Z.neg n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
now exists (Zpos n).exists p : Z,
  1%Z = (2 * p + (if Z.even 1 then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~1 =
  (2 * p + (if Z.even (Z.neg n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
now exists Z0.n:positive
exists p : Z,
  Z.neg n~1 =
  (2 * p + (if Z.even (Z.neg n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
exists (Zneg n - 1)%Z.n:positive
Z.neg n~1 =
(2 * (Z.neg n - 1) +
 (if Z.even (Z.neg n~1) then 0 else 1))%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
change (2 * Zneg n - 1 = 2 * (Zneg n - 1) + 1)%Z.n:positive
(2 * Z.neg n - 1)%Z = (2 * (Z.neg n - 1) + 1)%Z
n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
ring.n:positive
exists p : Z,
  Z.neg n~0 =
  (2 * p + (if Z.even (Z.neg n~0) then 0 else 1))%Z
exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
now exists (Zneg n).exists p : Z,
  (-1)%Z = (2 * p + (if Z.even (-1) then 0 else 1))%Z
now exists (-1)%Z.
Qed.

End Even_Odd.

Section Zpower.

Theorem Zpower_plus :
  forall n k1 k2, (0 <= k1)%Z -> (0 <= k2)%Z ->
  Zpower n (k1 + k2) = (Zpower n k1 * Zpower n k2)%Z.forall n k1 k2 : Z,
(0 <= k1)%Z ->
(0 <= k2)%Z -> (n ^ (k1 + k2))%Z = (n ^ k1 * n ^ k2)%Z
Proof.forall n k1 k2 : Z,
(0 <= k1)%Z ->
(0 <= k2)%Z -> (n ^ (k1 + k2))%Z = (n ^ k1 * n ^ k2)%Z
intros n k1 k2 H1 H2.n, k1, k2:Z
H1:(0 <= k1)%Z
H2:(0 <= k2)%Z
(n ^ (k1 + k2))%Z = (n ^ k1 * n ^ k2)%Z
now apply Zpower_exp ; apply Z.le_ge.
Qed.

Theorem Zpower_Zpower_nat :
  forall b e, (0 <= e)%Z ->
  Zpower b e = Zpower_nat b (Z.abs_nat e).forall b e : Z,
(0 <= e)%Z -> (b ^ e)%Z = Zpower_nat b (Z.abs_nat e)
Proof.forall b e : Z,
(0 <= e)%Z -> (b ^ e)%Z = Zpower_nat b (Z.abs_nat e)
intros b [|e|e] He.b:Z
He:(0 <= 0)%Z
(b ^ 0)%Z = Zpower_nat b (Z.abs_nat 0)
b:Z
e:positive
He:(0 <= Z.pos e)%Z
(b ^ Z.pos e)%Z = Zpower_nat b (Z.abs_nat (Z.pos e))
b:Z
e:positive
He:(0 <= Z.neg e)%Z
(b ^ Z.neg e)%Z = Zpower_nat b (Z.abs_nat (Z.neg e))
apply refl_equal.b:Z
e:positive
He:(0 <= Z.pos e)%Z
(b ^ Z.pos e)%Z = Zpower_nat b (Z.abs_nat (Z.pos e))
b:Z
e:positive
He:(0 <= Z.neg e)%Z
(b ^ Z.neg e)%Z = Zpower_nat b (Z.abs_nat (Z.neg e))
apply Zpower_pos_nat.b:Z
e:positive
He:(0 <= Z.neg e)%Z
(b ^ Z.neg e)%Z = Zpower_nat b (Z.abs_nat (Z.neg e))
elim He.b:Z
e:positive
He:(0 <= Z.neg e)%Z
(0 ?= Z.neg e)%Z = Gt
apply refl_equal.
Qed.

Theorem Zpower_nat_S :
  forall b e,
  Zpower_nat b (S e) = (b * Zpower_nat b e)%Z.forall (b : Z) (e : nat),
Zpower_nat b (S e) = (b * Zpower_nat b e)%Z
Proof.forall (b : Z) (e : nat),
Zpower_nat b (S e) = (b * Zpower_nat b e)%Z
intros b e.b:Z
e:nat
Zpower_nat b (S e) = (b * Zpower_nat b e)%Z
rewrite (Zpower_nat_is_exp 1 e).b:Z
e:nat
(Zpower_nat b 1 * Zpower_nat b e)%Z =
(b * Zpower_nat b e)%Z
apply (f_equal (fun x => x * _)%Z).b:Z
e:nat
Zpower_nat b 1 = b
apply Zmult_1_r.
Qed.

Theorem Zpower_pos_gt_0 :
  forall b p, (0 < b)%Z ->
  (0 < Zpower_pos b p)%Z.forall (b : Z) (p : positive),
(0 < b)%Z -> (0 < Z.pow_pos b p)%Z
Proof.forall (b : Z) (p : positive),
(0 < b)%Z -> (0 < Z.pow_pos b p)%Z
intros b p Hb.b:Z
p:positive
Hb:(0 < b)%Z
(0 < Z.pow_pos b p)%Z
rewrite Zpower_pos_nat.b:Z
p:positive
Hb:(0 < b)%Z
(0 < Zpower_nat b (Pos.to_nat p))%Z
induction (nat_of_P p).b:Z
p:positive
Hb:(0 < b)%Z
(0 < Zpower_nat b 0)%Z
b:Z
p:positive
Hb:(0 < b)%Z
n:nat
IHn:(0 < Zpower_nat b n)%Z
(0 < Zpower_nat b (S n))%Z
easy.b:Z
p:positive
Hb:(0 < b)%Z
n:nat
IHn:(0 < Zpower_nat b n)%Z
(0 < Zpower_nat b (S n))%Z
rewrite Zpower_nat_S.b:Z
p:positive
Hb:(0 < b)%Z
n:nat
IHn:(0 < Zpower_nat b n)%Z
(0 < b * Zpower_nat b n)%Z
now apply Zmult_lt_0_compat.
Qed.

Theorem Zeven_Zpower_odd :
  forall b e, (0 <= e)%Z -> Z.even b = false ->
  Z.even (Zpower b e) = false.forall b e : Z,
(0 <= e)%Z ->
Z.even b = false -> Z.even (b ^ e) = false
Proof.forall b e : Z,
(0 <= e)%Z ->
Z.even b = false -> Z.even (b ^ e) = false
intros b e He Hb.b, e:Z
He:(0 <= e)%Z
Hb:Z.even b = false
Z.even (b ^ e) = false
destruct (Z_le_lt_eq_dec _ _ He) as [He'|He'].b, e:Z
He:(0 <= e)%Z
Hb:Z.even b = false
He':(0 < e)%Z
Z.even (b ^ e) = false
b, e:Z
He:(0 <= e)%Z
Hb:Z.even b = false
He':0%Z = e
Z.even (b ^ e) = false
rewrite <- Hb.b, e:Z
He:(0 <= e)%Z
Hb:Z.even b = false
He':(0 < e)%Z
Z.even (b ^ e) = Z.even b
b, e:Z
He:(0 <= e)%Z
Hb:Z.even b = false
He':0%Z = e
Z.even (b ^ e) = false
now apply Z.even_pow.b, e:Z
He:(0 <= e)%Z
Hb:Z.even b = false
He':0%Z = e
Z.even (b ^ e) = false
now rewrite <- He'.
Qed.

The radix must be greater than 1

Record radix := { radix_val :> Z ; radix_prop : Zle_bool 2 radix_val = true }.

Theorem radix_val_inj :
  forall r1 r2, radix_val r1 = radix_val r2 -> r1 = r2.forall r1 r2 : radix, r1 = r2 -> r1 = r2
Proof.forall r1 r2 : radix, r1 = r2 -> r1 = r2
intros (r1, H1) (r2, H2) H.r1:Z
H1:(2 <=? r1)%Z = true
r2:Z
H2:(2 <=? r2)%Z = true
H:{| radix_val := r1; radix_prop := H1 |} =
{| radix_val := r2; radix_prop := H2 |}
{| radix_val := r1; radix_prop := H1 |} =
{| radix_val := r2; radix_prop := H2 |}
simpl in H.r1:Z
H1:(2 <=? r1)%Z = true
r2:Z
H2:(2 <=? r2)%Z = true
H:r1 = r2
{| radix_val := r1; radix_prop := H1 |} =
{| radix_val := r2; radix_prop := H2 |}
revert H1.r1, r2:Z
H2:(2 <=? r2)%Z = true
H:r1 = r2
forall H1 : (2 <=? r1)%Z = true,
{| radix_val := r1; radix_prop := H1 |} =
{| radix_val := r2; radix_prop := H2 |}
rewrite H.r1, r2:Z
H2:(2 <=? r2)%Z = true
H:r1 = r2
forall H1 : (2 <=? r2)%Z = true,
{| radix_val := r2; radix_prop := H1 |} =
{| radix_val := r2; radix_prop := H2 |}
intros H1.r1, r2:Z
H2:(2 <=? r2)%Z = true
H:r1 = r2
H1:(2 <=? r2)%Z = true
{| radix_val := r2; radix_prop := H1 |} =
{| radix_val := r2; radix_prop := H2 |}
apply f_equal.r1, r2:Z
H2:(2 <=? r2)%Z = true
H:r1 = r2
H1:(2 <=? r2)%Z = true
H1 = H2
apply eqbool_irrelevance.
Qed.

Definition radix2 := Build_radix 2 (refl_equal _).

Variable r : radix.

Theorem radix_gt_0 : (0 < r)%Z.r:radix
(0 < r)%Z
Proof.r:radix
(0 < r)%Z
apply Z.lt_le_trans with 2%Z.r:radix
(0 < 2)%Z
r:radix
(2 <= r)%Z
easy.r:radix
(2 <= r)%Z
apply Zle_bool_imp_le.r:radix
(2 <=? r)%Z = true
apply r.
Qed.

Theorem radix_gt_1 : (1 < r)%Z.r:radix
(1 < r)%Z
Proof.r:radix
(1 < r)%Z
destruct r as (v, Hr).r:radix
v:Z
Hr:(2 <=? v)%Z = true
(1 < {| radix_val := v; radix_prop := Hr |})%Z simpl.r:radix
v:Z
Hr:(2 <=? v)%Z = true
(1 < v)%Z
apply Z.lt_le_trans with 2%Z.r:radix
v:Z
Hr:(2 <=? v)%Z = true
(1 < 2)%Z
r:radix
v:Z
Hr:(2 <=? v)%Z = true
(2 <= v)%Z
easy.r:radix
v:Z
Hr:(2 <=? v)%Z = true
(2 <= v)%Z
now apply Zle_bool_imp_le.
Qed.

Theorem Zpower_gt_1 :
  forall p,
  (0 < p)%Z ->
  (1 < Zpower r p)%Z.r:radix
forall p : Z, (0 < p)%Z -> (1 < r ^ p)%Z
Proof.r:radix
forall p : Z, (0 < p)%Z -> (1 < r ^ p)%Z
intros [|p|p] Hp ; try easy.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
(1 < r ^ Z.pos p)%Z
simpl.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
(1 < Z.pow_pos r p)%Z
rewrite Zpower_pos_nat.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
(1 < Zpower_nat r (Pos.to_nat p))%Z
generalize (lt_O_nat_of_P p).r:radix
p:positive
Hp:(0 < Z.pos p)%Z
0 < Pos.to_nat p ->
(1 < Zpower_nat r (Pos.to_nat p))%Z
induction (nat_of_P p).r:radix
p:positive
Hp:(0 < Z.pos p)%Z
0 < 0 -> (1 < Zpower_nat r 0)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
0 < S n -> (1 < Zpower_nat r (S n))%Z
easy.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
0 < S n -> (1 < Zpower_nat r (S n))%Z
intros _.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
(1 < Zpower_nat r (S n))%Z
rewrite Zpower_nat_S.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
assert (0 < Zpower_nat r n)%Z.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
(0 < Zpower_nat r n)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
clear.r:radix
n:nat
(0 < Zpower_nat r n)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
induction n.r:radix
(0 < Zpower_nat r 0)%Z
r:radix
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < Zpower_nat r (S n))%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
easy.r:radix
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < Zpower_nat r (S n))%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
rewrite Zpower_nat_S.r:radix
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < r * Zpower_nat r n)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
apply Zmult_lt_0_compat with (2 := IHn).r:radix
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < r)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
apply radix_gt_0.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r * Zpower_nat r n)%Z
apply Z.le_lt_trans with (1 * Zpower_nat r n)%Z.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 <= 1 * Zpower_nat r n)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 * Zpower_nat r n < r * Zpower_nat r n)%Z
rewrite Zmult_1_l.r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 <= Zpower_nat r n)%Z
r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 * Zpower_nat r n < r * Zpower_nat r n)%Z
now apply (Zlt_le_succ 0).r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 * Zpower_nat r n < r * Zpower_nat r n)%Z
apply Zmult_lt_compat_r with (1 := H).r:radix
p:positive
Hp:(0 < Z.pos p)%Z
n:nat
IHn:0 < n -> (1 < Zpower_nat r n)%Z
H:(0 < Zpower_nat r n)%Z
(1 < r)%Z
apply radix_gt_1.
Qed.

Theorem Zpower_gt_0 :
  forall p,
  (0 <= p)%Z ->
  (0 < Zpower r p)%Z.r:radix
forall p : Z, (0 <= p)%Z -> (0 < r ^ p)%Z
Proof.r:radix
forall p : Z, (0 <= p)%Z -> (0 < r ^ p)%Z
intros p Hp.r:radix
p:Z
Hp:(0 <= p)%Z
(0 < r ^ p)%Z
rewrite Zpower_Zpower_nat with (1 := Hp).r:radix
p:Z
Hp:(0 <= p)%Z
(0 < Zpower_nat r (Z.abs_nat p))%Z
induction (Z.abs_nat p).r:radix
p:Z
Hp:(0 <= p)%Z
(0 < Zpower_nat r 0)%Z
r:radix
p:Z
Hp:(0 <= p)%Z
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < Zpower_nat r (S n))%Z
easy.r:radix
p:Z
Hp:(0 <= p)%Z
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < Zpower_nat r (S n))%Z
rewrite Zpower_nat_S.r:radix
p:Z
Hp:(0 <= p)%Z
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < r * Zpower_nat r n)%Z
apply Zmult_lt_0_compat with (2 := IHn).r:radix
p:Z
Hp:(0 <= p)%Z
n:nat
IHn:(0 < Zpower_nat r n)%Z
(0 < r)%Z
apply radix_gt_0.
Qed.

Theorem Zpower_ge_0 :
  forall e,
  (0 <= Zpower r e)%Z.r:radix
forall e : Z, (0 <= r ^ e)%Z
Proof.r:radix
forall e : Z, (0 <= r ^ e)%Z
intros [|e|e] ; try easy.r:radix
e:positive
(0 <= r ^ Z.pos e)%Z
apply Zlt_le_weak.r:radix
e:positive
(0 < r ^ Z.pos e)%Z
now apply Zpower_gt_0.
Qed.

Theorem Zpower_le :
  forall e1 e2, (e1 <= e2)%Z ->
  (Zpower r e1 <= Zpower r e2)%Z.r:radix
forall e1 e2 : Z, (e1 <= e2)%Z -> (r ^ e1 <= r ^ e2)%Z
Proof.r:radix
forall e1 e2 : Z, (e1 <= e2)%Z -> (r ^ e1 <= r ^ e2)%Z
intros e1 e2 He.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
(r ^ e1 <= r ^ e2)%Z
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 <= r ^ e2)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
replace e2 with (e2 - e1 + e1)%Z by ring.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 <= r ^ (e2 - e1 + e1))%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
rewrite Zpower_plus with (2 := H1).r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 <= r ^ (e2 - e1) * r ^ e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
rewrite <- (Zmult_1_l (r ^ e1)) at 1.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(1 * r ^ e1 <= r ^ (e2 - e1) * r ^ e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
apply Zmult_le_compat_r.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(1 <= r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= r ^ e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
apply (Zlt_le_succ 0).r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= r ^ e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
apply Zpower_gt_0.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= r ^ e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
now apply Zle_minus_le_0.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= r ^ e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
apply Zpower_ge_0.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
now apply Zle_minus_le_0.r:radix
e1, e2:Z
He:(e1 <= e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
clear He.r:radix
e1, e2:Z
H1:(e1 < 0)%Z
(r ^ e1 <= r ^ e2)%Z
destruct e1 as [|e1|e1] ; try easy.r:radix
e1:positive
e2:Z
H1:(Z.neg e1 < 0)%Z
(r ^ Z.neg e1 <= r ^ e2)%Z
apply Zpower_ge_0.
Qed.

Theorem Zpower_lt :
  forall e1 e2, (0 <= e2)%Z -> (e1 < e2)%Z ->
  (Zpower r e1 < Zpower r e2)%Z.r:radix
forall e1 e2 : Z,
(0 <= e2)%Z -> (e1 < e2)%Z -> (r ^ e1 < r ^ e2)%Z
Proof.r:radix
forall e1 e2 : Z,
(0 <= e2)%Z -> (e1 < e2)%Z -> (r ^ e1 < r ^ e2)%Z
intros e1 e2 He2 He.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
(r ^ e1 < r ^ e2)%Z
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 < r ^ e2)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
replace e2 with (e2 - e1 + e1)%Z by ring.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 < r ^ (e2 - e1 + e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
rewrite Zpower_plus with (2 := H1).r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 < r ^ (e2 - e1) * r ^ e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
rewrite Zmult_comm.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 < r ^ e1 * r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
rewrite <- (Zmult_1_r (r ^ e1)) at 1.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 * 1 < r ^ e1 * r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
apply Zmult_lt_compat2.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < r ^ e1 <= r ^ e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < 1 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
split.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < r ^ e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 <= r ^ e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < 1 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
now apply Zpower_gt_0.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(r ^ e1 <= r ^ e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < 1 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
apply Z.le_refl.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < 1 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
split.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < 1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(1 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
easy.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(1 < r ^ (e2 - e1))%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
apply Zpower_gt_1.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 < e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
clear -He ; omega.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(0 <= e2 - e1)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
apply Zle_minus_le_0.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(0 <= e1)%Z
(e1 <= e2)%Z
r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
now apply Zlt_le_weak.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
H1:(e1 < 0)%Z
(r ^ e1 < r ^ e2)%Z
revert H1.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
He:(e1 < e2)%Z
(e1 < 0)%Z -> (r ^ e1 < r ^ e2)%Z
clear -He2.r:radix
e1, e2:Z
He2:(0 <= e2)%Z
(e1 < 0)%Z -> (r ^ e1 < r ^ e2)%Z
destruct e1 ; try easy.r:radix
p:positive
e2:Z
He2:(0 <= e2)%Z
(Z.neg p < 0)%Z -> (r ^ Z.neg p < r ^ e2)%Z
intros _.r:radix
p:positive
e2:Z
He2:(0 <= e2)%Z
(r ^ Z.neg p < r ^ e2)%Z
now apply Zpower_gt_0.
Qed.

Theorem Zpower_lt_Zpower :
  forall e1 e2,
  (Zpower r (e1 - 1) < Zpower r e2)%Z ->
  (e1 <= e2)%Z.r:radix
forall e1 e2 : Z,
(r ^ (e1 - 1) < r ^ e2)%Z -> (e1 <= e2)%Z
Proof.r:radix
forall e1 e2 : Z,
(r ^ (e1 - 1) < r ^ e2)%Z -> (e1 <= e2)%Z
intros e1 e2 He.r:radix
e1, e2:Z
He:(r ^ (e1 - 1) < r ^ e2)%Z
(e1 <= e2)%Z
apply Znot_gt_le.r:radix
e1, e2:Z
He:(r ^ (e1 - 1) < r ^ e2)%Z
~ (e1 > e2)%Z
intros H.r:radix
e1, e2:Z
He:(r ^ (e1 - 1) < r ^ e2)%Z
H:(e1 > e2)%Z
False
apply Zlt_not_le with (1 := He).r:radix
e1, e2:Z
He:(r ^ (e1 - 1) < r ^ e2)%Z
H:(e1 > e2)%Z
(r ^ e2 <= r ^ (e1 - 1))%Z
apply Zpower_le.r:radix
e1, e2:Z
He:(r ^ (e1 - 1) < r ^ e2)%Z
H:(e1 > e2)%Z
(e2 <= e1 - 1)%Z
clear -H ; omega.
Qed.

Theorem Zpower_gt_id :
  forall n, (n < Zpower r n)%Z.r:radix
forall n : Z, (n < r ^ n)%Z
Proof.r:radix
forall n : Z, (n < r ^ n)%Z
intros [|n|n] ; try easy.r:radix
n:positive
(Z.pos n < r ^ Z.pos n)%Z
simpl.r:radix
n:positive
(Z.pos n < Z.pow_pos r n)%Z
rewrite Zpower_pos_nat.r:radix
n:positive
(Z.pos n < Zpower_nat r (Pos.to_nat n))%Z
rewrite Zpos_eq_Z_of_nat_o_nat_of_P.r:radix
n:positive
(Z.of_nat (Pos.to_nat n) < Zpower_nat r (Pos.to_nat n))%Z
induction (nat_of_P n).r:radix
n:positive
(Z.of_nat 0 < Zpower_nat r 0)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.of_nat (S n0) < Zpower_nat r (S n0))%Z
easy.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.of_nat (S n0) < Zpower_nat r (S n0))%Z
rewrite inj_S.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.succ (Z.of_nat n0) < Zpower_nat r (S n0))%Z
change (Zpower_nat r (S n0)) with (r * Zpower_nat r n0)%Z.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.succ (Z.of_nat n0) < r * Zpower_nat r n0)%Z
unfold Z.succ.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.of_nat n0 + 1 < r * Zpower_nat r n0)%Z
apply Z.lt_le_trans with (r * (Z_of_nat n0 + 1))%Z.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.of_nat n0 + 1 < r * (Z.of_nat n0 + 1))%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
clear.r:radix
n0:nat
(Z.of_nat n0 + 1 < r * (Z.of_nat n0 + 1))%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply Zlt_0_minus_lt.r:radix
n0:nat
(0 < r * (Z.of_nat n0 + 1) - (Z.of_nat n0 + 1))%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
replace (r * (Z_of_nat n0 + 1) - (Z_of_nat n0 + 1))%Z with ((r - 1) * (Z_of_nat n0 + 1))%Z by ring.r:radix
n0:nat
(0 < (r - 1) * (Z.of_nat n0 + 1))%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply Zmult_lt_0_compat.r:radix
n0:nat
(0 < r - 1)%Z
r:radix
n0:nat
(0 < Z.of_nat n0 + 1)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
cut (2 <= r)%Z.r:radix
n0:nat
(2 <= r)%Z -> (0 < r - 1)%Z
r:radix
n0:nat
(2 <= r)%Z
r:radix
n0:nat
(0 < Z.of_nat n0 + 1)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z omega.r:radix
n0:nat
(2 <= r)%Z
r:radix
n0:nat
(0 < Z.of_nat n0 + 1)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply Zle_bool_imp_le.r:radix
n0:nat
(2 <=? r)%Z = true
r:radix
n0:nat
(0 < Z.of_nat n0 + 1)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply r.r:radix
n0:nat
(0 < Z.of_nat n0 + 1)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply (Zle_lt_succ 0).r:radix
n0:nat
(0 <= Z.of_nat n0)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply Zle_0_nat.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(r * (Z.of_nat n0 + 1) <= r * Zpower_nat r n0)%Z
apply Zmult_le_compat_l.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(Z.of_nat n0 + 1 <= Zpower_nat r n0)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(0 <= r)%Z
now apply Zlt_le_succ.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(0 <= r)%Z
apply Z.le_trans with 2%Z.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(0 <= 2)%Z
r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(2 <= r)%Z
easy.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(2 <= r)%Z
apply Zle_bool_imp_le.r:radix
n:positive
n0:nat
IHn0:(Z.of_nat n0 < Zpower_nat r n0)%Z
(2 <=? r)%Z = true
apply r.
Qed.

End Zpower.

Section Div_Mod.

Theorem Zmod_mod_mult :
  forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
  Zmod (Zmod n (a * b)) b = Zmod n b.forall n a b : Z,
(0 < a)%Z ->
(0 <= b)%Z -> ((n mod (a * b)) mod b)%Z = (n mod b)%Z
Proof.forall n a b : Z,
(0 < a)%Z ->
(0 <= b)%Z -> ((n mod (a * b)) mod b)%Z = (n mod b)%Z
intros n a [|b|b] Ha Hb.n, a:Z
Ha:(0 < a)%Z
Hb:(0 <= 0)%Z
((n mod (a * 0)) mod 0)%Z = (n mod 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
((n mod (a * Z.pos b)) mod Z.pos b)%Z =
(n mod Z.pos b)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
now rewrite 2!Zmod_0_r.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
((n mod (a * Z.pos b)) mod Z.pos b)%Z =
(n mod Z.pos b)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
rewrite (Zmod_eq n (a * Zpos b)).n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
((n - n / (a * Z.pos b) * (a * Z.pos b)) mod Z.pos b)%Z =
(n mod Z.pos b)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a * Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
rewrite Zmult_assoc.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
((n - n / (a * Z.pos b) * a * Z.pos b) mod Z.pos b)%Z =
(n mod Z.pos b)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a * Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
unfold Zminus.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
((n + - (n / (a * Z.pos b) * a * Z.pos b)) mod Z.pos b)%Z =
(n mod Z.pos b)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a * Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
rewrite Zopp_mult_distr_l.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
((n + - (n / (a * Z.pos b) * a) * Z.pos b) mod Z.pos b)%Z =
(n mod Z.pos b)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a * Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
apply Z_mod_plus.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a * Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
easy.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a * Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
apply Zmult_gt_0_compat.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(a > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
now apply Z.lt_gt.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.pos b)%Z
(Z.pos b > 0)%Z
n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
easy.n, a:Z
b:positive
Ha:(0 < a)%Z
Hb:(0 <= Z.neg b)%Z
((n mod (a * Z.neg b)) mod Z.neg b)%Z =
(n mod Z.neg b)%Z
now elim Hb.
Qed.

Theorem ZOmod_eq :
  forall a b,
  Z.rem a b = (a - Z.quot a b * b)%Z.forall a b : Z, Z.rem a b = (a - a ÷ b * b)%Z
Proof.forall a b : Z, Z.rem a b = (a - a ÷ b * b)%Z
intros a b.a, b:Z
Z.rem a b = (a - a ÷ b * b)%Z
rewrite (Z.quot_rem' a b) at 2.a, b:Z
Z.rem a b = (b * (a ÷ b) + Z.rem a b - a ÷ b * b)%Z
ring.
Qed.

Theorem ZOmod_mod_mult :
  forall n a b,
  Z.rem (Z.rem n (a * b)) b = Z.rem n b.forall n a b : Z,
Z.rem (Z.rem n (a * b)) b = Z.rem n b
Proof.forall n a b : Z,
Z.rem (Z.rem n (a * b)) b = Z.rem n b
intros n a b.n, a, b:Z
Z.rem (Z.rem n (a * b)) b = Z.rem n b
assert (Z.rem n (a * b) = n + - (Z.quot n (a * b) * a) * b)%Z.n, a, b:Z
Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
Z.rem (Z.rem n (a * b)) b = Z.rem n b
rewrite <- Zopp_mult_distr_l.n, a, b:Z
Z.rem n (a * b) = (n + - (n ÷ (a * b) * a * b))%Z
n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
Z.rem (Z.rem n (a * b)) b = Z.rem n b
rewrite <- Zmult_assoc.n, a, b:Z
Z.rem n (a * b) = (n + - (n ÷ (a * b) * (a * b)))%Z
n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
Z.rem (Z.rem n (a * b)) b = Z.rem n b
apply ZOmod_eq.n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
Z.rem (Z.rem n (a * b)) b = Z.rem n b
rewrite H.n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
Z.rem (n + - (n ÷ (a * b) * a) * b) b = Z.rem n b
apply Z_rem_plus.n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
(0 <= (n + - (n ÷ (a * b) * a) * b) * n)%Z
rewrite <- H.n, a, b:Z
H:Z.rem n (a * b) = (n + - (n ÷ (a * b) * a) * b)%Z
(0 <= Z.rem n (a * b) * n)%Z
apply Zrem_sgn2.
Qed.

Theorem Zdiv_mod_mult :
  forall n a b, (0 <= a)%Z -> (0 <= b)%Z ->
  (Z.div (Zmod n (a * b)) a) = Zmod (Z.div n a) b.forall n a b : Z,
(0 <= a)%Z ->
(0 <= b)%Z ->
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
Proof.forall n a b : Z,
(0 <= a)%Z ->
(0 <= b)%Z ->
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
intros n a b Ha Hb.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|Hb'].n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite (Zmod_eq n (a * b)).n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
((n - n / (a * b) * (a * b)) / a)%Z =
((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite (Zmult_comm a b) at 2.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
((n - n / (a * b) * (b * a)) / a)%Z =
((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite Zmult_assoc.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
((n - n / (a * b) * b * a) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
unfold Zminus.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
((n + - (n / (a * b) * b * a)) / a)%Z =
((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite Zopp_mult_distr_l.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
((n + - (n / (a * b) * b) * a) / a)%Z =
((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite Z_div_plus by now apply Z.lt_gt.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(n / a + - (n / (a * b) * b))%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite <- Zdiv_Zdiv by easy.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(n / a + - (n / a / b * b))%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
apply sym_eq.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
((n / a) mod b)%Z = (n / a + - (n / a / b * b))%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
apply Zmod_eq.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
now apply Z.lt_gt.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':(0 < b)%Z
(a * b > 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
now apply Zmult_gt_0_compat ; apply Z.lt_gt.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite <- Hb'.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(n mod (a * 0) / a)%Z = ((n / a) mod 0)%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite Zmult_0_r, 2!Zmod_0_r.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':(0 < a)%Z
Hb':0%Z = b
(0 / a)%Z = 0%Z
n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
apply Zdiv_0_l.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (a * b) / a)%Z = ((n / a) mod b)%Z
rewrite <- Ha'.n, a, b:Z
Ha:(0 <= a)%Z
Hb:(0 <= b)%Z
Ha':0%Z = a
(n mod (0 * b) / 0)%Z = ((n / 0) mod b)%Z
now rewrite 2!Zdiv_0_r, Zmod_0_l.
Qed.

Theorem ZOdiv_mod_mult :
  forall n a b,
  (Z.quot (Z.rem n (a * b)) a) = Z.rem (Z.quot n a) b.forall n a b : Z,
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
Proof.forall n a b : Z,
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
intros n a b.n, a, b:Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
destruct (Z.eq_dec a 0) as [Za|Za].n, a, b:Z
Za:a = 0%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
n, a, b:Z
Za:a <> 0%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
rewrite Za.n, a, b:Z
Za:a = 0%Z
(Z.rem n (0 * b) ÷ 0)%Z = Z.rem (n ÷ 0) b
n, a, b:Z
Za:a <> 0%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
now rewrite 2!Zquot_0_r, Zrem_0_l.n, a, b:Z
Za:a <> 0%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
assert (Z.rem n (a * b) = n + - (Z.quot (Z.quot n a) b * b) * a)%Z.n, a, b:Z
Za:a <> 0%Z
Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
rewrite (ZOmod_eq n (a * b)) at 1.n, a, b:Z
Za:a <> 0%Z
(n - n ÷ (a * b) * (a * b))%Z =
(n + - (n ÷ a ÷ b * b) * a)%Z
n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
rewrite Zquot_Zquot.n, a, b:Z
Za:a <> 0%Z
(n - n ÷ (a * b) * (a * b))%Z =
(n + - (n ÷ (a * b) * b) * a)%Z
n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
ring.n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(Z.rem n (a * b) ÷ a)%Z = Z.rem (n ÷ a) b
rewrite H.n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
((n + - (n ÷ a ÷ b * b) * a) ÷ a)%Z = Z.rem (n ÷ a) b
rewrite Z_quot_plus with (2 := Za).n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(n ÷ a + - (n ÷ a ÷ b * b))%Z = Z.rem (n ÷ a) b
n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(0 <= (n + - (n ÷ a ÷ b * b) * a) * n)%Z
apply sym_eq.n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
Z.rem (n ÷ a) b = (n ÷ a + - (n ÷ a ÷ b * b))%Z
n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(0 <= (n + - (n ÷ a ÷ b * b) * a) * n)%Z
apply ZOmod_eq.n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(0 <= (n + - (n ÷ a ÷ b * b) * a) * n)%Z
rewrite <- H.n, a, b:Z
Za:a <> 0%Z
H:Z.rem n (a * b) = (n + - (n ÷ a ÷ b * b) * a)%Z
(0 <= Z.rem n (a * b) * n)%Z
apply Zrem_sgn2.
Qed.

Theorem ZOdiv_small_abs :
  forall a b,
  (Z.abs a < b)%Z -> Z.quot a b = Z0.forall a b : Z, (Z.abs a < b)%Z -> (a ÷ b)%Z = 0%Z
Proof.forall a b : Z, (Z.abs a < b)%Z -> (a ÷ b)%Z = 0%Z
intros a b Ha.a, b:Z
Ha:(Z.abs a < b)%Z
(a ÷ b)%Z = 0%Z
destruct (Zle_or_lt 0 a) as [H|H].a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(a ÷ b)%Z = 0%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(a ÷ b)%Z = 0%Z
apply Z.quot_small.a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(0 <= a < b)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(a ÷ b)%Z = 0%Z
split.a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(0 <= a)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(a < b)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(a ÷ b)%Z = 0%Z
exact H.a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(a < b)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(a ÷ b)%Z = 0%Z
now rewrite Z.abs_eq in Ha.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(a ÷ b)%Z = 0%Z
apply Z.opp_inj.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(- (a ÷ b))%Z = (- 0)%Z
rewrite <- Zquot_opp_l, Z.opp_0.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(- a ÷ b)%Z = 0%Z
apply Z.quot_small.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(0 <= - a < b)%Z
generalize (Zabs_non_eq a).a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
((a <= 0)%Z -> Z.abs a = (- a)%Z) -> (0 <= - a < b)%Z
omega.
Qed.

Theorem ZOmod_small_abs :
  forall a b,
  (Z.abs a < b)%Z -> Z.rem a b = a.forall a b : Z, (Z.abs a < b)%Z -> Z.rem a b = a
Proof.forall a b : Z, (Z.abs a < b)%Z -> Z.rem a b = a
intros a b Ha.a, b:Z
Ha:(Z.abs a < b)%Z
Z.rem a b = a
destruct (Zle_or_lt 0 a) as [H|H].a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
Z.rem a b = a
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
Z.rem a b = a
apply Z.rem_small.a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(0 <= a < b)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
Z.rem a b = a
split.a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(0 <= a)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(a < b)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
Z.rem a b = a
exact H.a, b:Z
Ha:(Z.abs a < b)%Z
H:(0 <= a)%Z
(a < b)%Z
a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
Z.rem a b = a
now rewrite Z.abs_eq in Ha.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
Z.rem a b = a
apply Z.opp_inj.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(- Z.rem a b)%Z = (- a)%Z
rewrite <- Zrem_opp_l.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
Z.rem (- a) b = (- a)%Z
apply Z.rem_small.a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
(0 <= - a < b)%Z
generalize (Zabs_non_eq a).a, b:Z
Ha:(Z.abs a < b)%Z
H:(a < 0)%Z
((a <= 0)%Z -> Z.abs a = (- a)%Z) -> (0 <= - a < b)%Z
omega.
Qed.

Theorem ZOdiv_plus :
  forall a b c, (0 <= a * b)%Z ->
  (Z.quot (a + b) c = Z.quot a c + Z.quot b c + Z.quot (Z.rem a c + Z.rem b c) c)%Z.forall a b c : Z,
(0 <= a * b)%Z ->
((a + b) ÷ c)%Z =
(a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c)%Z
Proof.forall a b c : Z,
(0 <= a * b)%Z ->
((a + b) ÷ c)%Z =
(a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c)%Z
intros a b c Hab.a, b, c:Z
Hab:(0 <= a * b)%Z
((a + b) ÷ c)%Z =
(a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c)%Z
destruct (Z.eq_dec c 0) as [Zc|Zc].a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c = 0%Z
((a + b) ÷ c)%Z =
(a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c)%Z
a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
((a + b) ÷ c)%Z =
(a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c)%Z
now rewrite Zc, 4!Zquot_0_r.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
((a + b) ÷ c)%Z =
(a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c)%Z
apply Zmult_reg_r with (1 := Zc).a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
((a + b) ÷ c * c)%Z =
((a ÷ c + b ÷ c + (Z.rem a c + Z.rem b c) ÷ c) * c)%Z
rewrite 2!Zmult_plus_distr_l.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
((a + b) ÷ c * c)%Z =
(a ÷ c * c + b ÷ c * c +
 (Z.rem a c + Z.rem b c) ÷ c * c)%Z
assert (forall d, Z.quot d c * c = d - Z.rem d c)%Z.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
H:forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
((a + b) ÷ c * c)%Z =
(a ÷ c * c + b ÷ c * c +
 (Z.rem a c + Z.rem b c) ÷ c * c)%Z
intros d.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
d:Z
(d ÷ c * c)%Z = (d - Z.rem d c)%Z
a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
H:forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
((a + b) ÷ c * c)%Z =
(a ÷ c * c + b ÷ c * c +
 (Z.rem a c + Z.rem b c) ÷ c * c)%Z
rewrite ZOmod_eq.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
d:Z
(d ÷ c * c)%Z = (d - (d - d ÷ c * c))%Z
a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
H:forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
((a + b) ÷ c * c)%Z =
(a ÷ c * c + b ÷ c * c +
 (Z.rem a c + Z.rem b c) ÷ c * c)%Z
ring.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
H:forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
((a + b) ÷ c * c)%Z =
(a ÷ c * c + b ÷ c * c +
 (Z.rem a c + Z.rem b c) ÷ c * c)%Z
rewrite 4!H.a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
H:forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
(a + b - Z.rem (a + b) c)%Z =
(a - Z.rem a c + (b - Z.rem b c) +
 (Z.rem a c + Z.rem b c -
  Z.rem (Z.rem a c + Z.rem b c) c))%Z
rewrite <- Zplus_rem with (1 := Hab).a, b, c:Z
Hab:(0 <= a * b)%Z
Zc:c <> 0%Z
H:forall d : Z, (d ÷ c * c)%Z = (d - Z.rem d c)%Z
(a + b - Z.rem (a + b) c)%Z =
(a - Z.rem a c + (b - Z.rem b c) +
 (Z.rem a c + Z.rem b c - Z.rem (a + b) c))%Z
ring.
Qed.

End Div_Mod.

Section Same_sign.

Theorem Zsame_sign_trans :
  forall v u w, v <> Z0 ->
  (0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z.forall v u w : Z,
v <> 0%Z ->
(0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z
Proof.forall v u w : Z,
v <> 0%Z ->
(0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now elim Zv.
Qed.

Theorem Zsame_sign_trans_weak :
  forall v u w, (v = Z0 -> w = Z0) ->
  (0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z.forall v u w : Z,
(v = 0%Z -> w = 0%Z) ->
(0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z
Proof.forall v u w : Z,
(v = 0%Z -> w = 0%Z) ->
(0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now discriminate Zv.
Qed.

Theorem Zsame_sign_imp :
  forall u v,
  (0 < u -> 0 <= v)%Z ->
  (0 < -u -> 0 <= -v)%Z ->
  (0 <= u * v)%Z.forall u v : Z,
((0 < u)%Z -> (0 <= v)%Z) ->
((0 < - u)%Z -> (0 <= - v)%Z) -> (0 <= u * v)%Z
Proof.forall u v : Z,
((0 < u)%Z -> (0 <= v)%Z) ->
((0 < - u)%Z -> (0 <= - v)%Z) -> (0 <= u * v)%Z
intros [|u|u] v Hp Hn.v:Z
Hp:(0 < 0)%Z -> (0 <= v)%Z
Hn:(0 < - 0)%Z -> (0 <= - v)%Z
(0 <= 0 * v)%Z
u:positive
v:Z
Hp:(0 < Z.pos u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.pos u)%Z -> (0 <= - v)%Z
(0 <= Z.pos u * v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.neg u * v)%Z
easy.u:positive
v:Z
Hp:(0 < Z.pos u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.pos u)%Z -> (0 <= - v)%Z
(0 <= Z.pos u * v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.neg u * v)%Z
apply Zmult_le_0_compat.u:positive
v:Z
Hp:(0 < Z.pos u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.pos u)%Z -> (0 <= - v)%Z
(0 <= Z.pos u)%Z
u:positive
v:Z
Hp:(0 < Z.pos u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.pos u)%Z -> (0 <= - v)%Z
(0 <= v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.neg u * v)%Z
easy.u:positive
v:Z
Hp:(0 < Z.pos u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.pos u)%Z -> (0 <= - v)%Z
(0 <= v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.neg u * v)%Z
now apply Hp.u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.neg u * v)%Z
replace (Zneg u * v)%Z with (Zpos u * (-v))%Z.u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.pos u * - v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(Z.pos u * - v)%Z = (Z.neg u * v)%Z
apply Zmult_le_0_compat.u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= Z.pos u)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= - v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(Z.pos u * - v)%Z = (Z.neg u * v)%Z
easy.u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(0 <= - v)%Z
u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(Z.pos u * - v)%Z = (Z.neg u * v)%Z
now apply Hn.u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(Z.pos u * - v)%Z = (Z.neg u * v)%Z
rewrite <- Zopp_mult_distr_r.u:positive
v:Z
Hp:(0 < Z.neg u)%Z -> (0 <= v)%Z
Hn:(0 < - Z.neg u)%Z -> (0 <= - v)%Z
(- (Z.pos u * v))%Z = (Z.neg u * v)%Z
apply Zopp_mult_distr_l.
Qed.

Theorem Zsame_sign_odiv :
  forall u v, (0 <= v)%Z ->
  (0 <= u * Z.quot u v)%Z.forall u v : Z, (0 <= v)%Z -> (0 <= u * (u ÷ v))%Z
Proof.forall u v : Z, (0 <= v)%Z -> (0 <= u * (u ÷ v))%Z
intros u v Hv.u, v:Z
Hv:(0 <= v)%Z
(0 <= u * (u ÷ v))%Z
apply Zsame_sign_imp ; intros Hu.u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < u)%Z
(0 <= u ÷ v)%Z
u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < - u)%Z
(0 <= - (u ÷ v))%Z
apply Z_quot_pos with (2 := Hv).u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < u)%Z
(0 <= u)%Z
u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < - u)%Z
(0 <= - (u ÷ v))%Z
now apply Zlt_le_weak.u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < - u)%Z
(0 <= - (u ÷ v))%Z
rewrite <- Zquot_opp_l.u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < - u)%Z
(0 <= - u ÷ v)%Z
apply Z_quot_pos with (2 := Hv).u, v:Z
Hv:(0 <= v)%Z
Hu:(0 < - u)%Z
(0 <= - u)%Z
now apply Zlt_le_weak.
Qed.

End Same_sign.

Boolean comparisons

Section Zeq_bool.

Inductive Zeq_bool_prop (x y : Z) : bool -> Prop :=
  | Zeq_bool_true_ : x = y -> Zeq_bool_prop x y true
  | Zeq_bool_false_ : x <> y -> Zeq_bool_prop x y false.

Theorem Zeq_bool_spec :
  forall x y, Zeq_bool_prop x y (Zeq_bool x y).forall x y : Z, Zeq_bool_prop x y (Zeq_bool x y)
Proof.forall x y : Z, Zeq_bool_prop x y (Zeq_bool x y)
intros x y.x, y:Z
Zeq_bool_prop x y (Zeq_bool x y)
generalize (Zeq_is_eq_bool x y).x, y:Z
x = y <-> Zeq_bool x y = true ->
Zeq_bool_prop x y (Zeq_bool x y)
case (Zeq_bool x y) ; intros (H1, H2) ; constructor.x, y:Z
H1:x = y -> true = true
H2:true = true -> x = y
x = y
x, y:Z
H1:x = y -> false = true
H2:false = true -> x = y
x <> y
now apply H2.x, y:Z
H1:x = y -> false = true
H2:false = true -> x = y
x <> y
intros H.x, y:Z
H1:x = y -> false = true
H2:false = true -> x = y
H:x = y
False
specialize (H1 H).x, y:Z
H1:false = true
H2:false = true -> x = y
H:x = y
False
discriminate H1.
Qed.

Theorem Zeq_bool_true :
  forall x y, x = y -> Zeq_bool x y = true.forall x y : Z, x = y -> Zeq_bool x y = true
Proof.forall x y : Z, x = y -> Zeq_bool x y = true
intros x y.x, y:Z
x = y -> Zeq_bool x y = true
apply -> Zeq_is_eq_bool.
Qed.

Theorem Zeq_bool_false :
  forall x y, x <> y -> Zeq_bool x y = false.forall x y : Z, x <> y -> Zeq_bool x y = false
Proof.forall x y : Z, x <> y -> Zeq_bool x y = false
intros x y.x, y:Z
x <> y -> Zeq_bool x y = false
generalize (proj2 (Zeq_is_eq_bool x y)).x, y:Z
(Zeq_bool x y = true -> x = y) ->
x <> y -> Zeq_bool x y = false
case Zeq_bool.x, y:Z
(true = true -> x = y) -> x <> y -> true = false
x, y:Z
(false = true -> x = y) -> x <> y -> false = false
intros He Hn.x, y:Z
He:true = true -> x = y
Hn:x <> y
true = false
x, y:Z
(false = true -> x = y) -> x <> y -> false = false
elim Hn.x, y:Z
He:true = true -> x = y
Hn:x <> y
x = y
x, y:Z
(false = true -> x = y) -> x <> y -> false = false
now apply He.x, y:Z
(false = true -> x = y) -> x <> y -> false = false
now intros _ _.
Qed.

End Zeq_bool.

Section Zle_bool.

Inductive Zle_bool_prop (x y : Z) : bool -> Prop :=
  | Zle_bool_true_ : (x <= y)%Z -> Zle_bool_prop x y true
  | Zle_bool_false_ : (y < x)%Z -> Zle_bool_prop x y false.

Theorem Zle_bool_spec :
  forall x y, Zle_bool_prop x y (Zle_bool x y).forall x y : Z, Zle_bool_prop x y (x <=? y)%Z
Proof.forall x y : Z, Zle_bool_prop x y (x <=? y)%Z
intros x y.x, y:Z
Zle_bool_prop x y (x <=? y)%Z
generalize (Zle_is_le_bool x y).x, y:Z
(x <= y)%Z <-> (x <=? y)%Z = true ->
Zle_bool_prop x y (x <=? y)%Z
case Zle_bool ; intros (H1, H2) ; constructor.x, y:Z
H1:(x <= y)%Z -> true = true
H2:true = true -> (x <= y)%Z
(x <= y)%Z
x, y:Z
H1:(x <= y)%Z -> false = true
H2:false = true -> (x <= y)%Z
(y < x)%Z
now apply H2.x, y:Z
H1:(x <= y)%Z -> false = true
H2:false = true -> (x <= y)%Z
(y < x)%Z
destruct (Zle_or_lt x y) as [H|H].x, y:Z
H1:(x <= y)%Z -> false = true
H2:false = true -> (x <= y)%Z
H:(x <= y)%Z
(y < x)%Z
x, y:Z
H1:(x <= y)%Z -> false = true
H2:false = true -> (x <= y)%Z
H:(y < x)%Z
(y < x)%Z
now specialize (H1 H).x, y:Z
H1:(x <= y)%Z -> false = true
H2:false = true -> (x <= y)%Z
H:(y < x)%Z
(y < x)%Z
exact H.
Qed.

Theorem Zle_bool_true :
  forall x y : Z,
  (x <= y)%Z -> Zle_bool x y = true.forall x y : Z, (x <= y)%Z -> (x <=? y)%Z = true
Proof.forall x y : Z, (x <= y)%Z -> (x <=? y)%Z = true
intros x y.x, y:Z
(x <= y)%Z -> (x <=? y)%Z = true
apply (proj1 (Zle_is_le_bool x y)).
Qed.

Theorem Zle_bool_false :
  forall x y : Z,
  (y < x)%Z -> Zle_bool x y = false.forall x y : Z, (y < x)%Z -> (x <=? y)%Z = false
Proof.forall x y : Z, (y < x)%Z -> (x <=? y)%Z = false
intros x y Hxy.x, y:Z
Hxy:(y < x)%Z
(x <=? y)%Z = false
generalize (Zle_cases x y).x, y:Z
Hxy:(y < x)%Z
(if (x <=? y)%Z then (x <= y)%Z else (x > y)%Z) ->
(x <=? y)%Z = false
case Zle_bool ; intros H.x, y:Z
Hxy:(y < x)%Z
H:(x <= y)%Z
true = false
x, y:Z
Hxy:(y < x)%Z
H:(x > y)%Z
false = false
elim (Z.lt_irrefl x).x, y:Z
Hxy:(y < x)%Z
H:(x <= y)%Z
(x < x)%Z
x, y:Z
Hxy:(y < x)%Z
H:(x > y)%Z
false = false
now apply Z.le_lt_trans with y.x, y:Z
Hxy:(y < x)%Z
H:(x > y)%Z
false = false
apply refl_equal.
Qed.

End Zle_bool.

Section Zlt_bool.

Inductive Zlt_bool_prop (x y : Z) : bool -> Prop :=
  | Zlt_bool_true_ : (x < y)%Z -> Zlt_bool_prop x y true
  | Zlt_bool_false_ : (y <= x)%Z -> Zlt_bool_prop x y false.

Theorem Zlt_bool_spec :
  forall x y, Zlt_bool_prop x y (Zlt_bool x y).forall x y : Z, Zlt_bool_prop x y (x <? y)%Z
Proof.forall x y : Z, Zlt_bool_prop x y (x <? y)%Z
intros x y.x, y:Z
Zlt_bool_prop x y (x <? y)%Z
generalize (Zlt_is_lt_bool x y).x, y:Z
(x < y)%Z <-> (x <? y)%Z = true ->
Zlt_bool_prop x y (x <? y)%Z
case Zlt_bool ; intros (H1, H2) ; constructor.x, y:Z
H1:(x < y)%Z -> true = true
H2:true = true -> (x < y)%Z
(x < y)%Z
x, y:Z
H1:(x < y)%Z -> false = true
H2:false = true -> (x < y)%Z
(y <= x)%Z
now apply H2.x, y:Z
H1:(x < y)%Z -> false = true
H2:false = true -> (x < y)%Z
(y <= x)%Z
destruct (Zle_or_lt y x) as [H|H].x, y:Z
H1:(x < y)%Z -> false = true
H2:false = true -> (x < y)%Z
H:(y <= x)%Z
(y <= x)%Z
x, y:Z
H1:(x < y)%Z -> false = true
H2:false = true -> (x < y)%Z
H:(x < y)%Z
(y <= x)%Z
exact H.x, y:Z
H1:(x < y)%Z -> false = true
H2:false = true -> (x < y)%Z
H:(x < y)%Z
(y <= x)%Z
now specialize (H1 H).
Qed.

Theorem Zlt_bool_true :
  forall x y : Z,
  (x < y)%Z -> Zlt_bool x y = true.forall x y : Z, (x < y)%Z -> (x <? y)%Z = true
Proof.forall x y : Z, (x < y)%Z -> (x <? y)%Z = true
intros x y.x, y:Z
(x < y)%Z -> (x <? y)%Z = true
apply (proj1 (Zlt_is_lt_bool x y)).
Qed.

Theorem Zlt_bool_false :
  forall x y : Z,
  (y <= x)%Z -> Zlt_bool x y = false.forall x y : Z, (y <= x)%Z -> (x <? y)%Z = false
Proof.forall x y : Z, (y <= x)%Z -> (x <? y)%Z = false
intros x y Hxy.x, y:Z
Hxy:(y <= x)%Z
(x <? y)%Z = false
generalize (Zlt_cases x y).x, y:Z
Hxy:(y <= x)%Z
(if (x <? y)%Z then (x < y)%Z else (x >= y)%Z) ->
(x <? y)%Z = false
case Zlt_bool ; intros H.x, y:Z
Hxy:(y <= x)%Z
H:(x < y)%Z
true = false
x, y:Z
Hxy:(y <= x)%Z
H:(x >= y)%Z
false = false
elim (Z.lt_irrefl x).x, y:Z
Hxy:(y <= x)%Z
H:(x < y)%Z
(x < x)%Z
x, y:Z
Hxy:(y <= x)%Z
H:(x >= y)%Z
false = false
now apply Z.lt_le_trans with y.x, y:Z
Hxy:(y <= x)%Z
H:(x >= y)%Z
false = false
apply refl_equal.
Qed.

Theorem negb_Zle_bool :
  forall x y : Z,
  negb (Zle_bool x y) = Zlt_bool y x.forall x y : Z, negb (x <=? y)%Z = (y <? x)%Z
Proof.forall x y : Z, negb (x <=? y)%Z = (y <? x)%Z
intros x y.x, y:Z
negb (x <=? y)%Z = (y <? x)%Z
case Zle_bool_spec ; intros H.x, y:Z
H:(x <= y)%Z
negb true = (y <? x)%Z
x, y:Z
H:(y < x)%Z
negb false = (y <? x)%Z
now rewrite Zlt_bool_false.x, y:Z
H:(y < x)%Z
negb false = (y <? x)%Z
now rewrite Zlt_bool_true.
Qed.

Theorem negb_Zlt_bool :
  forall x y : Z,
  negb (Zlt_bool x y) = Zle_bool y x.forall x y : Z, negb (x <? y)%Z = (y <=? x)%Z
Proof.forall x y : Z, negb (x <? y)%Z = (y <=? x)%Z
intros x y.x, y:Z
negb (x <? y)%Z = (y <=? x)%Z
case Zlt_bool_spec ; intros H.x, y:Z
H:(x < y)%Z
negb true = (y <=? x)%Z
x, y:Z
H:(y <= x)%Z
negb false = (y <=? x)%Z
now rewrite Zle_bool_false.x, y:Z
H:(y <= x)%Z
negb false = (y <=? x)%Z
now rewrite Zle_bool_true.
Qed.

End Zlt_bool.

Section Zcompare.

Inductive Zcompare_prop (x y : Z) : comparison -> Prop :=
  | Zcompare_Lt_ : (x < y)%Z -> Zcompare_prop x y Lt
  | Zcompare_Eq_ : x = y -> Zcompare_prop x y Eq
  | Zcompare_Gt_ : (y < x)%Z -> Zcompare_prop x y Gt.

Theorem Zcompare_spec :
  forall x y, Zcompare_prop x y (Z.compare x y).forall x y : Z, Zcompare_prop x y (x ?= y)%Z
Proof.forall x y : Z, Zcompare_prop x y (x ?= y)%Z
intros x y.x, y:Z
Zcompare_prop x y (x ?= y)%Z
destruct (Z_dec x y) as [[H|H]|H].x, y:Z
H:(x < y)%Z
Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:(x > y)%Z
Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
generalize (Zlt_compare _ _ H).x, y:Z
H:(x < y)%Z
match (x ?= y)%Z with
| Lt => True
| _ => False
end -> Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:(x > y)%Z
Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
case (Z.compare x y) ; try easy.x, y:Z
H:(x < y)%Z
True -> Zcompare_prop x y Lt
x, y:Z
H:(x > y)%Z
Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
now constructor.x, y:Z
H:(x > y)%Z
Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
generalize (Zgt_compare _ _ H).x, y:Z
H:(x > y)%Z
match (x ?= y)%Z with
| Gt => True
| _ => False
end -> Zcompare_prop x y (x ?= y)%Z
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
case (Z.compare x y) ; try easy.x, y:Z
H:(x > y)%Z
True -> Zcompare_prop x y Gt
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
constructor.x, y:Z
H:(x > y)%Z
H0:True
(y < x)%Z
x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
now apply Z.gt_lt.x, y:Z
H:x = y
Zcompare_prop x y (x ?= y)%Z
generalize (proj2 (Zcompare_Eq_iff_eq _ _) H).x, y:Z
H:x = y
(x ?= y)%Z = Eq -> Zcompare_prop x y (x ?= y)%Z
case (Z.compare x y) ; try easy.x, y:Z
H:x = y
Eq = Eq -> Zcompare_prop x y Eq
now constructor.
Qed.

Theorem Zcompare_Lt :
  forall x y,
  (x < y)%Z -> Z.compare x y = Lt.forall x y : Z, (x < y)%Z -> (x ?= y)%Z = Lt
Proof.forall x y : Z, (x < y)%Z -> (x ?= y)%Z = Lt
easy.
Qed.

Theorem Zcompare_Eq :
  forall x y,
  (x = y)%Z -> Z.compare x y = Eq.forall x y : Z, x = y -> (x ?= y)%Z = Eq
Proof.forall x y : Z, x = y -> (x ?= y)%Z = Eq
intros x y.x, y:Z
x = y -> (x ?= y)%Z = Eq
apply <- Zcompare_Eq_iff_eq.
Qed.

Theorem Zcompare_Gt :
  forall x y,
  (y < x)%Z -> Z.compare x y = Gt.forall x y : Z, (y < x)%Z -> (x ?= y)%Z = Gt
Proof.forall x y : Z, (y < x)%Z -> (x ?= y)%Z = Gt
intros x y.x, y:Z
(y < x)%Z -> (x ?= y)%Z = Gt
apply Z.lt_gt.
Qed.

End Zcompare.

Section cond_Zopp.

Theorem cond_Zopp_negb :
  forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y).forall (x : bool) (y : Z),
SpecFloatCopy.cond_Zopp (negb x) y =
(- SpecFloatCopy.cond_Zopp x y)%Z
Proof.forall (x : bool) (y : Z),
SpecFloatCopy.cond_Zopp (negb x) y =
(- SpecFloatCopy.cond_Zopp x y)%Z
intros [|] y.y:Z
SpecFloatCopy.cond_Zopp (negb true) y =
(- SpecFloatCopy.cond_Zopp true y)%Z
y:Z
SpecFloatCopy.cond_Zopp (negb false) y =
(- SpecFloatCopy.cond_Zopp false y)%Z
apply sym_eq, Z.opp_involutive.y:Z
SpecFloatCopy.cond_Zopp (negb false) y =
(- SpecFloatCopy.cond_Zopp false y)%Z
easy.
Qed.

Theorem abs_cond_Zopp :
  forall b m,
  Z.abs (cond_Zopp b m) = Z.abs m.forall (b : bool) (m : Z),
Z.abs (SpecFloatCopy.cond_Zopp b m) = Z.abs m
Proof.forall (b : bool) (m : Z),
Z.abs (SpecFloatCopy.cond_Zopp b m) = Z.abs m
intros [|] m.m:Z
Z.abs (SpecFloatCopy.cond_Zopp true m) = Z.abs m
m:Z
Z.abs (SpecFloatCopy.cond_Zopp false m) = Z.abs m
apply Zabs_Zopp.m:Z
Z.abs (SpecFloatCopy.cond_Zopp false m) = Z.abs m
apply refl_equal.
Qed.

Theorem cond_Zopp_Zlt_bool :
  forall m,
  cond_Zopp (Zlt_bool m 0) m = Z.abs m.forall m : Z,
SpecFloatCopy.cond_Zopp (m <? 0)%Z m = Z.abs m
Proof.forall m : Z,
SpecFloatCopy.cond_Zopp (m <? 0)%Z m = Z.abs m
intros m.m:Z
SpecFloatCopy.cond_Zopp (m <? 0)%Z m = Z.abs m
apply sym_eq.m:Z
Z.abs m = SpecFloatCopy.cond_Zopp (m <? 0)%Z m
case Zlt_bool_spec ; intros Hm.m:Z
Hm:(m < 0)%Z
Z.abs m = SpecFloatCopy.cond_Zopp true m
m:Z
Hm:(0 <= m)%Z
Z.abs m = SpecFloatCopy.cond_Zopp false m
apply Zabs_non_eq.m:Z
Hm:(m < 0)%Z
(m <= 0)%Z
m:Z
Hm:(0 <= m)%Z
Z.abs m = SpecFloatCopy.cond_Zopp false m
now apply Zlt_le_weak.m:Z
Hm:(0 <= m)%Z
Z.abs m = SpecFloatCopy.cond_Zopp false m
now apply Z.abs_eq.
Qed.

End cond_Zopp.

Section fast_pow_pos.

Fixpoint Zfast_pow_pos (v : Z) (e : positive) : Z :=
  match e with
  | xH => v
  | xO e' => Z.square (Zfast_pow_pos v e')
  | xI e' => Zmult v (Z.square (Zfast_pow_pos v e'))
  end.

Theorem Zfast_pow_pos_correct :
  forall v e, Zfast_pow_pos v e = Zpower_pos v e.forall (v : Z) (e : positive),
Zfast_pow_pos v e = Z.pow_pos v e
Proof.forall (v : Z) (e : positive),
Zfast_pow_pos v e = Z.pow_pos v e
intros v e.v:Z
e:positive
Zfast_pow_pos v e = Z.pow_pos v e
rewrite <- (Zmult_1_r (Zfast_pow_pos v e)).v:Z
e:positive
(Zfast_pow_pos v e * 1)%Z = Z.pow_pos v e
unfold Z.pow_pos.v:Z
e:positive
(Zfast_pow_pos v e * 1)%Z = Pos.iter (Z.mul v) 1%Z e
generalize 1%Z.v:Z
e:positive
forall z : Z,
(Zfast_pow_pos v e * z)%Z = Pos.iter (Z.mul v) z e
revert v.e:positive
forall v z : Z,
(Zfast_pow_pos v e * z)%Z = Pos.iter (Z.mul v) z e
induction e ; intros v f ; simpl.e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(v * Z.square (Zfast_pow_pos v e) * f)%Z =
(v * Pos.iter (Z.mul v) (Pos.iter (Z.mul v) f e) e)%Z
e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(Z.square (Zfast_pow_pos v e) * f)%Z =
Pos.iter (Z.mul v) (Pos.iter (Z.mul v) f e) e
v, f:Z
(v * f)%Z = (v * f)%Z
-e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(v * Z.square (Zfast_pow_pos v e) * f)%Z =
(v * Pos.iter (Z.mul v) (Pos.iter (Z.mul v) f e) e)%Z rewrite <- 2!IHe.e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(v * Z.square (Zfast_pow_pos v e) * f)%Z =
(v * (Zfast_pow_pos v e * (Zfast_pow_pos v e * f)))%Z
  rewrite Z.square_spec.e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(v * (Zfast_pow_pos v e * Zfast_pow_pos v e) * f)%Z =
(v * (Zfast_pow_pos v e * (Zfast_pow_pos v e * f)))%Z
  ring.
-e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(Z.square (Zfast_pow_pos v e) * f)%Z =
Pos.iter (Z.mul v) (Pos.iter (Z.mul v) f e) e rewrite <- 2!IHe.e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(Z.square (Zfast_pow_pos v e) * f)%Z =
(Zfast_pow_pos v e * (Zfast_pow_pos v e * f))%Z
  rewrite Z.square_spec.e:positive
IHe:forall v0 z : Z, (Zfast_pow_pos v0 e * z)%Z = Pos.iter (Z.mul v0) z e
v, f:Z
(Zfast_pow_pos v e * Zfast_pow_pos v e * f)%Z =
(Zfast_pow_pos v e * (Zfast_pow_pos v e * f))%Z
  apply eq_sym, Zmult_assoc.
-v, f:Z
(v * f)%Z = (v * f)%Z apply eq_refl.
Qed.

End fast_pow_pos.

Section faster_div.

Lemma Zdiv_eucl_unique :
  forall a b,
  Z.div_eucl a b = (Z.div a b, Zmod a b).forall a b : Z,
Z.div_eucl a b = ((a / b)%Z, (a mod b)%Z)
Proof.forall a b : Z,
Z.div_eucl a b = ((a / b)%Z, (a mod b)%Z)
intros a b.a, b:Z
Z.div_eucl a b = ((a / b)%Z, (a mod b)%Z)
unfold Z.div, Zmod.a, b:Z
Z.div_eucl a b =
(let (q, _) := Z.div_eucl a b in q,
let (_, r) := Z.div_eucl a b in r)
now case Z.div_eucl.
Qed.

Fixpoint Zpos_div_eucl_aux1 (a b : positive) {struct b} :=
  match b with
  | xO b' =>
    match a with
    | xO a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r)%Z
    | xI a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r + 1)%Z
    | xH => (Z0, Zpos a)
    end
  | xH => (Zpos a, Z0)
  | xI _ => Z.pos_div_eucl a (Zpos b)
  end.

Lemma Zpos_div_eucl_aux1_correct :
  forall a b,
  Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Zpos b).forall a b : positive,
Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Z.pos b)
Proof.forall a b : positive,
Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Z.pos b)
intros a b.a, b:positive
Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Z.pos b)
revert a.b:positive
forall a : positive,
Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Z.pos b)
induction b ; intros a.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~1 =
Z.pos_div_eucl a (Z.pos b~1)
b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
Z.pos_div_eucl a (Z.pos b~0)
a:positive
Zpos_div_eucl_aux1 a 1 = Z.pos_div_eucl a 1
-b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~1 =
Z.pos_div_eucl a (Z.pos b~1) easy.
-b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
Z.pos_div_eucl a (Z.pos b~0) change (Z.pos_div_eucl a (Zpos b~0)) with (Z.div_eucl (Zpos a) (Zpos b~0)).b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
Z.div_eucl (Z.pos a) (Z.pos b~0)
  rewrite Zdiv_eucl_unique.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
((Z.pos a / Z.pos b~0)%Z, (Z.pos a mod Z.pos b~0)%Z)
  change (Zpos b~0) with (2 * Zpos b)%Z.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
((Z.pos a / (2 * Z.pos b))%Z,
(Z.pos a mod (2 * Z.pos b))%Z)
  rewrite Z.rem_mul_r by easy.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
((Z.pos a / (2 * Z.pos b))%Z,
(Z.pos a mod 2 + 2 * ((Z.pos a / 2) mod Z.pos b))%Z)
  rewrite <- Zdiv_Zdiv by easy.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a b~0 =
((Z.pos a / 2 / Z.pos b)%Z,
(Z.pos a mod 2 + 2 * ((Z.pos a / 2) mod Z.pos b))%Z)
  destruct a as [a|a|].b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a~1 b~0 =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z)
b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a~0 b~0 =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z)
b:positive
IHb:forall a : positive, Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Z.pos b)
Zpos_div_eucl_aux1 1 b~0 =
((1 / 2 / Z.pos b)%Z,
(1 mod 2 + 2 * ((1 / 2) mod Z.pos b))%Z)
  +b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a~1 b~0 =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z) change (Zpos_div_eucl_aux1 a~1 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r + 1)%Z).b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
(let (q, r) := Zpos_div_eucl_aux1 a b in
 (q, (2 * r + 1)%Z)) =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z)
    rewrite IHb.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
(let (q, r) := Z.pos_div_eucl a (Z.pos b) in
 (q, (2 * r + 1)%Z)) =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z) clear IHb.b, a:positive
(let (q, r) := Z.pos_div_eucl a (Z.pos b) in
 (q, (2 * r + 1)%Z)) =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z)
    change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).b, a:positive
(let (q, r) := Z.div_eucl (Z.pos a) (Z.pos b) in
 (q, (2 * r + 1)%Z)) =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z)
    rewrite Zdiv_eucl_unique.b, a:positive
((Z.pos a / Z.pos b)%Z,
(2 * (Z.pos a mod Z.pos b) + 1)%Z) =
((Z.pos a~1 / 2 / Z.pos b)%Z,
(Z.pos a~1 mod 2 + 2 * ((Z.pos a~1 / 2) mod Z.pos b))%Z)
    change (Zpos a~1) with (1 + 2 * Zpos a)%Z.b, a:positive
((Z.pos a / Z.pos b)%Z,
(2 * (Z.pos a mod Z.pos b) + 1)%Z) =
(((1 + 2 * Z.pos a) / 2 / Z.pos b)%Z,
((1 + 2 * Z.pos a) mod 2 +
 2 * (((1 + 2 * Z.pos a) / 2) mod Z.pos b))%Z)
    rewrite (Zmult_comm 2 (Zpos a)).b, a:positive
((Z.pos a / Z.pos b)%Z,
(2 * (Z.pos a mod Z.pos b) + 1)%Z) =
(((1 + Z.pos a * 2) / 2 / Z.pos b)%Z,
((1 + Z.pos a * 2) mod 2 +
 2 * (((1 + Z.pos a * 2) / 2) mod Z.pos b))%Z)
    rewrite Z_div_plus_full by easy.b, a:positive
((Z.pos a / Z.pos b)%Z,
(2 * (Z.pos a mod Z.pos b) + 1)%Z) =
(((1 / 2 + Z.pos a) / Z.pos b)%Z,
((1 + Z.pos a * 2) mod 2 +
 2 * ((1 / 2 + Z.pos a) mod Z.pos b))%Z)
    apply f_equal.b, a:positive
(2 * (Z.pos a mod Z.pos b) + 1)%Z =
((1 + Z.pos a * 2) mod 2 +
 2 * ((1 / 2 + Z.pos a) mod Z.pos b))%Z
    rewrite Z_mod_plus_full.b, a:positive
(2 * (Z.pos a mod Z.pos b) + 1)%Z =
(1 mod 2 + 2 * ((1 / 2 + Z.pos a) mod Z.pos b))%Z
    apply Zplus_comm.
  +b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
Zpos_div_eucl_aux1 a~0 b~0 =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z) change (Zpos_div_eucl_aux1 a~0 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r)%Z).b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
(let (q, r) := Zpos_div_eucl_aux1 a b in
 (q, (2 * r)%Z)) =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z)
    rewrite IHb.b:positive
IHb:forall a0 : positive, Zpos_div_eucl_aux1 a0 b = Z.pos_div_eucl a0 (Z.pos b)
a:positive
(let (q, r) := Z.pos_div_eucl a (Z.pos b) in
 (q, (2 * r)%Z)) =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z) clear IHb.b, a:positive
(let (q, r) := Z.pos_div_eucl a (Z.pos b) in
 (q, (2 * r)%Z)) =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z)
    change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).b, a:positive
(let (q, r) := Z.div_eucl (Z.pos a) (Z.pos b) in
 (q, (2 * r)%Z)) =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z)
    rewrite Zdiv_eucl_unique.b, a:positive
((Z.pos a / Z.pos b)%Z, (2 * (Z.pos a mod Z.pos b))%Z) =
((Z.pos a~0 / 2 / Z.pos b)%Z,
(Z.pos a~0 mod 2 + 2 * ((Z.pos a~0 / 2) mod Z.pos b))%Z)
    change (Zpos a~0) with (2 * Zpos a)%Z.b, a:positive
((Z.pos a / Z.pos b)%Z, (2 * (Z.pos a mod Z.pos b))%Z) =
((2 * Z.pos a / 2 / Z.pos b)%Z,
((2 * Z.pos a) mod 2 +
 2 * ((2 * Z.pos a / 2) mod Z.pos b))%Z)
    rewrite (Zmult_comm 2 (Zpos a)).b, a:positive
((Z.pos a / Z.pos b)%Z, (2 * (Z.pos a mod Z.pos b))%Z) =
((Z.pos a * 2 / 2 / Z.pos b)%Z,
((Z.pos a * 2) mod 2 +
 2 * ((Z.pos a * 2 / 2) mod Z.pos b))%Z)
    rewrite Z_div_mult_full by easy.b, a:positive
((Z.pos a / Z.pos b)%Z, (2 * (Z.pos a mod Z.pos b))%Z) =
((Z.pos a / Z.pos b)%Z,
((Z.pos a * 2) mod 2 + 2 * (Z.pos a mod Z.pos b))%Z)
    apply f_equal.b, a:positive
(2 * (Z.pos a mod Z.pos b))%Z =
((Z.pos a * 2) mod 2 + 2 * (Z.pos a mod Z.pos b))%Z
    now rewrite Z_mod_mult.
  +b:positive
IHb:forall a : positive, Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Z.pos b)
Zpos_div_eucl_aux1 1 b~0 =
((1 / 2 / Z.pos b)%Z,
(1 mod 2 + 2 * ((1 / 2) mod Z.pos b))%Z) easy.
-a:positive
Zpos_div_eucl_aux1 a 1 = Z.pos_div_eucl a 1 change (Z.pos_div_eucl a 1) with (Z.div_eucl (Zpos a) 1).a:positive
Zpos_div_eucl_aux1 a 1 = Z.div_eucl (Z.pos a) 1
  rewrite Zdiv_eucl_unique.a:positive
Zpos_div_eucl_aux1 a 1 =
((Z.pos a / 1)%Z, (Z.pos a mod 1)%Z)
  now rewrite Zdiv_1_r, Zmod_1_r.
Qed.

Definition Zpos_div_eucl_aux (a b : positive) :=
  match Pos.compare a b with
  | Lt => (Z0, Zpos a)
  | Eq => (1%Z, Z0)
  | Gt => Zpos_div_eucl_aux1 a b
  end.

Lemma Zpos_div_eucl_aux_correct :
  forall a b,
  Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Zpos b).forall a b : positive,
Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Z.pos b)
Proof.forall a b : positive,
Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Z.pos b)
intros a b.a, b:positive
Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Z.pos b)
unfold Zpos_div_eucl_aux.a, b:positive
match (a ?= b)%positive with
| Eq => (1%Z, 0%Z)
| Lt => (0%Z, Z.pos a)
| Gt => Zpos_div_eucl_aux1 a b
end = Z.pos_div_eucl a (Z.pos b)
change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).a, b:positive
match (a ?= b)%positive with
| Eq => (1%Z, 0%Z)
| Lt => (0%Z, Z.pos a)
| Gt => Zpos_div_eucl_aux1 a b
end = Z.div_eucl (Z.pos a) (Z.pos b)
rewrite Zdiv_eucl_unique.a, b:positive
match (a ?= b)%positive with
| Eq => (1%Z, 0%Z)
| Lt => (0%Z, Z.pos a)
| Gt => Zpos_div_eucl_aux1 a b
end = ((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
case Pos.compare_spec ; intros H.a, b:positive
H:a = b
(1%Z, 0%Z) =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
a, b:positive
H:(a < b)%positive
(0%Z, Z.pos a) =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
a, b:positive
H:(b < a)%positive
Zpos_div_eucl_aux1 a b =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
now rewrite H, Z_div_same, Z_mod_same.a, b:positive
H:(a < b)%positive
(0%Z, Z.pos a) =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
a, b:positive
H:(b < a)%positive
Zpos_div_eucl_aux1 a b =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
now rewrite Zdiv_small, Zmod_small by (split ; easy).a, b:positive
H:(b < a)%positive
Zpos_div_eucl_aux1 a b =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
rewrite Zpos_div_eucl_aux1_correct.a, b:positive
H:(b < a)%positive
Z.pos_div_eucl a (Z.pos b) =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).a, b:positive
H:(b < a)%positive
Z.div_eucl (Z.pos a) (Z.pos b) =
((Z.pos a / Z.pos b)%Z, (Z.pos a mod Z.pos b)%Z)
apply Zdiv_eucl_unique.
Qed.

Definition Zfast_div_eucl (a b : Z) :=
  match a with
  | Z0 => (0, 0)%Z
  | Zpos a' =>
    match b with
    | Z0 => (0, 0)%Z
    | Zpos b' => Zpos_div_eucl_aux a' b'
    | Zneg b' =>
      let (q, r) := Zpos_div_eucl_aux a' b' in
      match r with
      | Z0 => (-q, 0)%Z
      | Zpos _ => (-(q + 1), (b + r))%Z
      | Zneg _ => (-(q + 1), (b + r))%Z
      end
    end
  | Zneg a' =>
    match b with
    | Z0 => (0, 0)%Z
    | Zpos b' =>
      let (q, r) := Zpos_div_eucl_aux a' b' in
      match r with
      | Z0 => (-q, 0)%Z
      | Zpos _ => (-(q + 1), (b - r))%Z
      | Zneg _ => (-(q + 1), (b - r))%Z
      end
    | Zneg b' => let (q, r) := Zpos_div_eucl_aux a' b' in (q, (-r)%Z)
    end
  end.

Theorem Zfast_div_eucl_correct :
  forall a b : Z,
  Zfast_div_eucl a b = Z.div_eucl a b.forall a b : Z, Zfast_div_eucl a b = Z.div_eucl a b
Proof.forall a b : Z, Zfast_div_eucl a b = Z.div_eucl a b
unfold Zfast_div_eucl.forall a b : Z,
match a with
| 0%Z => (0%Z, 0%Z)
| Z.pos a' =>
    match b with
    | 0%Z => (0%Z, 0%Z)
    | Z.pos b' => Zpos_div_eucl_aux a' b'
    | Z.neg b' =>
        let (q, r) := Zpos_div_eucl_aux a' b' in
        match r with
        | 0%Z => ((- q)%Z, 0%Z)
        | _ => ((- (q + 1))%Z, (b + r)%Z)
        end
    end
| Z.neg a' =>
    match b with
    | 0%Z => (0%Z, 0%Z)
    | Z.pos b' =>
        let (q, r) := Zpos_div_eucl_aux a' b' in
        match r with
        | 0%Z => ((- q)%Z, 0%Z)
        | _ => ((- (q + 1))%Z, (b - r)%Z)
        end
    | Z.neg b' =>
        let (q, r) := Zpos_div_eucl_aux a' b' in
        (q, (- r)%Z)
    end
end = Z.div_eucl a b
intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy.
Qed.

End faster_div.

Section Iter.

Context {A : Type}.
Variable (f : A -> A).

Fixpoint iter_nat (n : nat) (x : A) {struct n} : A :=
  match n with
  | S n' => iter_nat n' (f x)
  | O => x
  end.

Lemma iter_nat_plus :
  forall (p q : nat) (x : A),
  iter_nat (p + q) x = iter_nat p (iter_nat q x).A:Type
f:A -> A
forall (p q : nat) (x : A),
iter_nat (p + q) x = iter_nat p (iter_nat q x)
Proof.A:Type
f:A -> A
forall (p q : nat) (x : A),
iter_nat (p + q) x = iter_nat p (iter_nat q x)
induction q.A:Type
f:A -> A
p:nat
forall x : A,
iter_nat (p + 0) x = iter_nat p (iter_nat 0 x)
A:Type
f:A -> A
p, q:nat
IHq:forall x : A, iter_nat (p + q) x = iter_nat p (iter_nat q x)
forall x : A,
iter_nat (p + S q) x = iter_nat p (iter_nat (S q) x)
now rewrite plus_0_r.A:Type
f:A -> A
p, q:nat
IHq:forall x : A, iter_nat (p + q) x = iter_nat p (iter_nat q x)
forall x : A,
iter_nat (p + S q) x = iter_nat p (iter_nat (S q) x)
intros x.A:Type
f:A -> A
p, q:nat
IHq:forall x0 : A, iter_nat (p + q) x0 = iter_nat p (iter_nat q x0)
x:A
iter_nat (p + S q) x = iter_nat p (iter_nat (S q) x)
rewrite <- plus_n_Sm.A:Type
f:A -> A
p, q:nat
IHq:forall x0 : A, iter_nat (p + q) x0 = iter_nat p (iter_nat q x0)
x:A
iter_nat (S (p + q)) x = iter_nat p (iter_nat (S q) x)
apply IHq.
Qed.

Lemma iter_nat_S :
  forall (p : nat) (x : A),
  iter_nat (S p) x = f (iter_nat p x).A:Type
f:A -> A
forall (p : nat) (x : A),
iter_nat (S p) x = f (iter_nat p x)
Proof.A:Type
f:A -> A
forall (p : nat) (x : A),
iter_nat (S p) x = f (iter_nat p x)
induction p.A:Type
f:A -> A
forall x : A, iter_nat 1 x = f (iter_nat 0 x)
A:Type
f:A -> A
p:nat
IHp:forall x : A, iter_nat (S p) x = f (iter_nat p x)
forall x : A,
iter_nat (S (S p)) x = f (iter_nat (S p) x)
easy.A:Type
f:A -> A
p:nat
IHp:forall x : A, iter_nat (S p) x = f (iter_nat p x)
forall x : A,
iter_nat (S (S p)) x = f (iter_nat (S p) x)
simpl.A:Type
f:A -> A
p:nat
IHp:forall x : A, iter_nat (S p) x = f (iter_nat p x)
forall x : A,
iter_nat p (f (f x)) = f (iter_nat p (f x))
intros x.A:Type
f:A -> A
p:nat
IHp:forall x0 : A, iter_nat (S p) x0 = f (iter_nat p x0)
x:A
iter_nat p (f (f x)) = f (iter_nat p (f x))
apply IHp.
Qed.

Lemma iter_pos_nat :
  forall (p : positive) (x : A),
  iter_pos f p x = iter_nat (Pos.to_nat p) x.A:Type
f:A -> A
forall (p : positive) (x : A),
SpecFloatCopy.iter_pos f p x =
iter_nat (Pos.to_nat p) x
Proof.A:Type
f:A -> A
forall (p : positive) (x : A),
SpecFloatCopy.iter_pos f p x =
iter_nat (Pos.to_nat p) x
induction p ; intros x.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~1 x =
iter_nat (Pos.to_nat p~1) x
A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite Pos2Nat.inj_xI.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~1 x =
iter_nat (S (2 * Pos.to_nat p)) x
A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
simpl.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (SpecFloatCopy.iter_pos f p (f x)) =
iter_nat (Pos.to_nat p + (Pos.to_nat p + 0)) (f x)
A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite plus_0_r.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (SpecFloatCopy.iter_pos f p (f x)) =
iter_nat (Pos.to_nat p + Pos.to_nat p) (f x)
A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite iter_nat_plus.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (SpecFloatCopy.iter_pos f p (f x)) =
iter_nat (Pos.to_nat p)
  (iter_nat (Pos.to_nat p) (f x))
A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite (IHp (f x)).A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (iter_nat (Pos.to_nat p) (f x)) =
iter_nat (Pos.to_nat p)
  (iter_nat (Pos.to_nat p) (f x))
A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
apply IHp.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (Pos.to_nat p~0) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite Pos2Nat.inj_xO.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p~0 x =
iter_nat (2 * Pos.to_nat p) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
simpl.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (SpecFloatCopy.iter_pos f p x) =
iter_nat (Pos.to_nat p + (Pos.to_nat p + 0)) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite plus_0_r.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (SpecFloatCopy.iter_pos f p x) =
iter_nat (Pos.to_nat p + Pos.to_nat p) x
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite iter_nat_plus.A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p
  (SpecFloatCopy.iter_pos f p x) =
iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) x)
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
rewrite (IHp x).A:Type
f:A -> A
p:positive
IHp:forall x0 : A, SpecFloatCopy.iter_pos f p x0 = iter_nat (Pos.to_nat p) x0
x:A
SpecFloatCopy.iter_pos f p (iter_nat (Pos.to_nat p) x) =
iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) x)
A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
apply IHp.A:Type
f:A -> A
x:A
SpecFloatCopy.iter_pos f 1 x =
iter_nat (Pos.to_nat 1) x
easy.
Qed.

End Iter.