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/
Copyright (C) 2011-2018 Sylvie Boldo
Copyright (C) 2011-2018 Guillaume Melquiond
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 Zquot.

Require Import Zaux.
Require Import SpecFloatCompat.

Notation digits2_pos := digits2_pos (only parsing).
Notation Zdigits2 := Zdigits2 (only parsing).
Number of bits (radix 2) of a positive integer.
It serves as an upper bound on the number of digits to ensure termination.
Fixpoint digits2_Pnat (n : positive) : nat :=
  match n with
  | xH => O
  | xO p => S (digits2_Pnat p)
  | xI p => S (digits2_Pnat p)
  end.


forall n : positive, let d := digits2_Pnat n in (Zpower_nat 2 d <= Z.pos n < Zpower_nat 2 (S d))%Z

forall n : positive, let d := digits2_Pnat n in (Zpower_nat 2 d <= Z.pos n < Zpower_nat 2 (S d))%Z
n:positive
d:=digits2_Pnat n:nat

(Zpower_nat 2 d <= Z.pos n < Zpower_nat 2 (S d))%Z
n:positive
d:=digits2_Pnat n:nat

(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z
n:positive

(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z

(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
IHn:(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z

(Zpower_nat 2 (S (digits2_Pnat n)) <= Z.pos n~1 < Zpower_nat 2 (S (S (digits2_Pnat n))))%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
IHn:(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z
(Zpower_nat 2 (S (digits2_Pnat n)) <= Z.pos n~0 < Zpower_nat 2 (S (S (digits2_Pnat n))))%Z
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
(Zpower_nat 2 0 <= 1 < Zpower_nat 2 1)%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
IHn:(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z

(2 * Zpower_nat 2 (digits2_Pnat n) <= 2 * Z.pos n + 1 < 2 * Zpower_nat 2 (S (digits2_Pnat n)))%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
IHn:(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z
(Zpower_nat 2 (S (digits2_Pnat n)) <= Z.pos n~0 < Zpower_nat 2 (S (S (digits2_Pnat n))))%Z
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
(Zpower_nat 2 0 <= 1 < Zpower_nat 2 1)%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
IHn:(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z

(Zpower_nat 2 (S (digits2_Pnat n)) <= Z.pos n~0 < Zpower_nat 2 (S (S (digits2_Pnat n))))%Z
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
(Zpower_nat 2 0 <= 1 < Zpower_nat 2 1)%Z
n:positive
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
IHn:(Zpower_nat 2 (digits2_Pnat n) <= Z.pos n < Zpower_nat 2 (S (digits2_Pnat n)))%Z

(2 * Zpower_nat 2 (digits2_Pnat n) <= 2 * Z.pos n < 2 * Zpower_nat 2 (S (digits2_Pnat n)))%Z
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z
(Zpower_nat 2 0 <= 1 < Zpower_nat 2 1)%Z
Hp:forall m : nat, Zpower_nat 2 (S m) = (2 * Zpower_nat 2 m)%Z

(Zpower_nat 2 0 <= 1 < Zpower_nat 2 1)%Z
now split. Qed. Section Fcore_digits. Variable beta : radix. Definition Zdigit n k := Z.rem (Z.quot n (Zpower beta k)) beta.
beta:radix

forall n k : Z, (k < 0)%Z -> Zdigit n k = 0%Z
beta:radix

forall n k : Z, (k < 0)%Z -> Zdigit n k = 0%Z
beta:radix
n:Z
k:positive
Hk:(Z.neg k < 0)%Z

Zdigit n (Z.neg k) = 0%Z
now case n. Qed.
beta:radix

forall k : Z, Zdigit 0 k = 0%Z
beta:radix

forall k : Z, Zdigit 0 k = 0%Z
beta:radix
k:Z

Zdigit 0 k = 0%Z
beta:radix
k:Z

Z.rem (0 ÷ beta ^ k) beta = 0%Z
beta:radix
k:Z

Z.rem 0 beta = 0%Z
apply Zrem_0_l. Qed.
beta:radix

forall n k : Z, Zdigit (- n) k = (- Zdigit n k)%Z
beta:radix

forall n k : Z, Zdigit (- n) k = (- Zdigit n k)%Z
beta:radix
n, k:Z

Zdigit (- n) k = (- Zdigit n k)%Z
beta:radix
n, k:Z

Z.rem (- n ÷ beta ^ k) beta = (- Z.rem (n ÷ beta ^ k) beta)%Z
beta:radix
n, k:Z

Z.rem (- (n ÷ beta ^ k)) beta = (- Z.rem (n ÷ beta ^ k) beta)%Z
apply Zrem_opp_l. Qed.
beta:radix

forall e n : Z, (0 <= n < beta ^ e)%Z -> forall k : Z, (e <= k)%Z -> Zdigit n k = 0%Z
beta:radix

forall e n : Z, (0 <= n < beta ^ e)%Z -> forall k : Z, (e <= k)%Z -> Zdigit n k = 0%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

Zdigit n k = 0%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

Z.rem (n ÷ beta ^ k) beta = 0%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

Z.rem 0 beta = 0%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= n < beta ^ k)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 <= n < beta ^ k)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 <= n)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(n < beta ^ k)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(n < beta ^ k)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(beta ^ e <= beta ^ k)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(beta ^ e <= beta ^ (e + (k - e)))%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(beta ^ e <= beta ^ e * beta ^ (k - e))%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(beta ^ e * 1 <= beta ^ e * beta ^ (k - e))%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(1 <= beta ^ (k - e))%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= beta ^ e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 < beta ^ (k - e))%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= beta ^ e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= beta ^ e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 <= beta ^ e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 < beta ^ e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 < beta ^ e)%Z -> (0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e:Z

(0 < beta ^ e)%Z -> (0 <= e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z
(0 <= k - e)%Z
beta:radix
e, n:Z
Hn:(0 <= n < beta ^ e)%Z
k:Z
Hk:(e <= k)%Z

(0 <= k - e)%Z
now apply Zle_minus_le_0. Qed.
beta:radix

forall e n : Z, (Z.abs n < beta ^ e)%Z -> forall k : Z, (e <= k)%Z -> Zdigit n k = 0%Z
beta:radix

forall e n : Z, (Z.abs n < beta ^ e)%Z -> forall k : Z, (e <= k)%Z -> Zdigit n k = 0%Z
beta:radix
e:Z
Hn:(Z.abs 0 < beta ^ e)%Z
k:Z

(e <= k)%Z -> Zdigit 0 k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.pos n) < beta ^ e)%Z
k:Z
(e <= k)%Z -> Zdigit (Z.pos n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
(e <= k)%Z -> Zdigit (Z.neg n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.pos n) < beta ^ e)%Z
k:Z

(e <= k)%Z -> Zdigit (Z.pos n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
(e <= k)%Z -> Zdigit (Z.neg n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.pos n) < beta ^ e)%Z
k:Z

(0 <= Z.pos n < beta ^ e)%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
(e <= k)%Z -> Zdigit (Z.neg n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z

(e <= k)%Z -> Zdigit (Z.neg n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
He:(e <= k)%Z

Zdigit (Z.neg n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
He:(e <= k)%Z

Zdigit (- Z.pos n) k = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
He:(e <= k)%Z

(- Zdigit (Z.pos n) k)%Z = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
He:(e <= k)%Z

(- 0)%Z = 0%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
He:(e <= k)%Z
(0 <= Z.pos n < beta ^ e)%Z
beta:radix
e:Z
n:positive
Hn:(Z.abs (Z.neg n) < beta ^ e)%Z
k:Z
He:(e <= k)%Z

(0 <= Z.pos n < beta ^ e)%Z
now split. Qed.
beta:radix

forall e n : Z, (0 <= e)%Z -> (beta ^ e <= n < beta ^ (e + 1))%Z -> Zdigit n e <> 0%Z
beta:radix

forall e n : Z, (0 <= e)%Z -> (beta ^ e <= n < beta ^ (e + 1))%Z -> Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

Z.rem (n ÷ beta ^ e) beta <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(Z.rem n (beta ^ e * beta) ÷ beta ^ e)%Z <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(n ÷ beta ^ e)%Z <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

False
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

(n < beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

(beta ^ e * (n ÷ beta ^ e) + Z.rem n (beta ^ e) < beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

(Z.rem n (beta ^ e) < beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

(0 <= n)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z
(0 < beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

(0 <= beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z
(0 < beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
H:(n ÷ beta ^ e)%Z = 0%Z

(0 < beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(0 <= n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(0 <= n)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(0 <= beta ^ e)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(n < beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(n < beta ^ (e + 1))%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z
(beta ^ (e + 1))%Z = (beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(beta ^ (e + 1))%Z = (beta ^ e * beta)%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn1:(beta ^ e <= n)%Z
Hn2:(n < beta ^ (e + 1))%Z

(beta ^ (e + 1))%Z = (beta ^ e * (beta * 1))%Z
now apply (Zpower_plus beta e 1). Qed.
beta:radix

forall e n : Z, (0 <= e)%Z -> (beta ^ e <= Z.abs n < beta ^ (e + 1))%Z -> Zdigit n e <> 0%Z
beta:radix

forall e n : Z, (0 <= e)%Z -> (beta ^ e <= Z.abs n < beta ^ (e + 1))%Z -> Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= Z.abs n < beta ^ (e + 1))%Z

Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= Z.abs n < beta ^ (e + 1))%Z
Hn':(0 <= n)%Z

Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= Z.abs n < beta ^ (e + 1))%Z
Hn':(n < 0)%Z
Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= n < beta ^ (e + 1))%Z
Hn':(0 <= n)%Z

Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= Z.abs n < beta ^ (e + 1))%Z
Hn':(n < 0)%Z
Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= Z.abs n < beta ^ (e + 1))%Z
Hn':(n < 0)%Z

Zdigit n e <> 0%Z
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= Z.abs n < beta ^ (e + 1))%Z
Hn':(n < 0)%Z
H:Zdigit n e = 0%Z

False
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= - n < beta ^ (e + 1))%Z
Hn':(n < 0)%Z
H:Zdigit n e = 0%Z

False
beta:radix
e, n:Z
He:(0 <= e)%Z
Hn:(beta ^ e <= - n < beta ^ (e + 1))%Z
Hn':(n < 0)%Z
H:Zdigit n e = 0%Z

Zdigit (- n) e = 0%Z
now rewrite Zdigit_opp, H. Qed.
beta:radix

forall n k k' : Z, (0 <= k')%Z -> Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix

forall n k k' : Z, (0 <= k')%Z -> Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z

Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k' <= k)%Z

Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
Hk':(0 <= k')%Z

forall k : Z, (k' <= k)%Z -> Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
Hk':(0 <= k')%Z

forall x : Z, (forall y : Z, (0 <= y < x)%Z -> forall k : Z, (y <= k)%Z -> Zdigit (n * beta ^ y) k = Zdigit n (k - y)) -> (0 <= x)%Z -> forall k : Z, (x <= k)%Z -> Zdigit (n * beta ^ x) k = Zdigit n (k - x)
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n:Z

forall x : Z, (forall y : Z, (0 <= y < x)%Z -> forall k : Z, (y <= k)%Z -> Zdigit (n * beta ^ y) k = Zdigit n (k - y)) -> (0 <= x)%Z -> forall k : Z, (x <= k)%Z -> Zdigit (n * beta ^ x) k = Zdigit n (k - x)
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

Z.rem (n * beta ^ k' ÷ beta ^ k) beta = Z.rem (n ÷ beta ^ (k - k')) beta
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

(n * beta ^ k' ÷ beta ^ k)%Z = (n ÷ beta ^ (k - k'))%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

(n * beta ^ k' ÷ beta ^ (k - k' + k'))%Z = (n ÷ beta ^ (k - k'))%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

(n * beta ^ k' ÷ (beta ^ (k - k') * beta ^ k'))%Z = (n ÷ beta ^ (k - k'))%Z
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z
(0 <= k - k')%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

(beta ^ k')%Z <> 0%Z
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z
(0 <= k - k')%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

(0 < beta ^ k')%Z
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z
(0 <= k - k')%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k':Z
IHk':forall y : Z, (0 <= y < k')%Z -> forall k0 : Z, (y <= k0)%Z -> Zdigit (n * beta ^ y) k0 = Zdigit n (k0 - y)
Hk':(0 <= k')%Z
k:Z
H:(k' <= k)%Z

(0 <= k - k')%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z

Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Zdigit (n * beta ^ k') k = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ k' ÷ beta ^ k) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ (k' - k + k) ÷ beta ^ k) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * (beta ^ (k' - k) * beta ^ k) ÷ beta ^ k) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ (k' - k)) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ (k' - k - 1 + 1)) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * (beta ^ (k' - k - 1) * beta ^ 1)) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ (k' - k - 1) * beta ^ 1) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ (k' - k - 1) * (beta * 1)) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

Z.rem (n * beta ^ (k' - k - 1) * beta) beta = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

(beta ^ k)%Z <> 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

(0 < beta ^ k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z
(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

(0 <= k' - k)%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(0 <= k)%Z

(k <= k')%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z
Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z

Zdigit (n * beta ^ k') k = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z

0%Z = Zdigit n (k - k')
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z

Zdigit n (k - k') = 0%Z
beta:radix
n, k, k':Z
Hk':(0 <= k')%Z
H:(k < k')%Z
H0:(k < 0)%Z

(k - k' < 0)%Z
omega. Qed.
beta:radix

forall n k k' : Z, (0 <= k)%Z -> (0 <= k')%Z -> Zdigit (n ÷ beta ^ k') k = Zdigit n (k + k')
beta:radix

forall n k k' : Z, (0 <= k)%Z -> (0 <= k')%Z -> Zdigit (n ÷ beta ^ k') k = Zdigit n (k + k')
beta:radix
n, k, k':Z
Hk:(0 <= k)%Z
Hk':(0 <= k')%Z

Zdigit (n ÷ beta ^ k') k = Zdigit n (k + k')
beta:radix
n, k, k':Z
Hk:(0 <= k)%Z
Hk':(0 <= k')%Z

Z.rem (n ÷ beta ^ k' ÷ beta ^ k) beta = Z.rem (n ÷ beta ^ (k + k')) beta
beta:radix
n, k, k':Z
Hk:(0 <= k)%Z
Hk':(0 <= k')%Z

Z.rem (n ÷ (beta ^ k' * beta ^ k)) beta = Z.rem (n ÷ beta ^ (k + k')) beta
beta:radix
n, k, k':Z
Hk:(0 <= k)%Z
Hk':(0 <= k')%Z

Z.rem (n ÷ (beta ^ k' * beta ^ k)) beta = Z.rem (n ÷ beta ^ (k' + k)) beta
now rewrite Zpower_plus. Qed.
beta:radix

forall n k k' : Z, (k < k')%Z -> Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix

forall n k k' : Z, (k < k')%Z -> Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z

Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ k') ÷ beta ^ k) beta = Z.rem (n ÷ beta ^ k) beta
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

(Z.rem (Z.rem n (beta ^ k')) (beta ^ k * beta) ÷ beta ^ k)%Z = (Z.rem n (beta ^ k * beta) ÷ beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ k')) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ (k + 1 + (k' - (k + 1))))) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ (k + 1) * beta ^ (k' - (k + 1)))) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ (k' - (k + 1)) * beta ^ (k + 1))) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ (k' - (k + 1)) * (beta ^ k * beta ^ 1))) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ (k' - (k + 1)) * (beta ^ k * (beta * 1)))) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(0 <= k)%Z

Z.rem (Z.rem n (beta ^ (k' - (k + 1)) * (beta ^ k * beta))) (beta ^ k * beta) = Z.rem n (beta ^ k * beta)
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z
Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
beta:radix
n, k, k':Z
Hk:(k < k')%Z
H:(k < 0)%Z

Zdigit (Z.rem n (beta ^ k')) k = Zdigit n k
now rewrite 2!Zdigit_lt. Qed.
beta:radix

forall n k k' : Z, (0 <= k' <= k)%Z -> Zdigit (Z.rem n (beta ^ k')) k = 0%Z
beta:radix

forall n k k' : Z, (0 <= k' <= k)%Z -> Zdigit (Z.rem n (beta ^ k')) k = 0%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

Zdigit (Z.rem n (beta ^ k')) k = 0%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

Z.rem (Z.rem n (beta ^ k') ÷ beta ^ k) beta = 0%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

Z.rem 0 beta = 0%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z
(Z.abs (Z.rem n (beta ^ k')) < beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

(Z.abs (Z.rem n (beta ^ k')) < beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

(Z.abs (Z.rem n (beta ^ k')) < beta ^ k')%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z
(beta ^ k' <= beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

(Z.abs (Z.rem n (beta ^ k')) < Z.abs (beta ^ k'))%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z
(beta ^ k' <= beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

(beta ^ k')%Z <> 0%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z
(beta ^ k' <= beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

(0 < beta ^ k')%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z
(beta ^ k' <= beta ^ k)%Z
beta:radix
n, k, k':Z
Hk:(0 <= k' <= k)%Z

(beta ^ k' <= beta ^ k)%Z
now apply Zpower_le. Qed. Fixpoint Zsum_digit f k := match k with | O => Z0 | S k => (Zsum_digit f k + f (Z_of_nat k) * Zpower beta (Z_of_nat k))%Z end.
beta:radix

forall (n : Z) (k : nat), Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
beta:radix

forall (n : Z) (k : nat), Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
beta:radix
n:Z

forall k : nat, Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
beta:radix
n:Z

Zsum_digit (Zdigit n) 0 = Z.rem n (beta ^ Z.of_nat 0)
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
Zsum_digit (Zdigit n) (S k) = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z

Z.rem n (beta ^ Z.of_nat 0) = Zsum_digit (Zdigit n) 0
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
Zsum_digit (Zdigit n) (S k) = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

Zsum_digit (Zdigit n) (S k) = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Zsum_digit (Zdigit n) k + Zdigit n (Z.of_nat k) * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Z.rem n (beta ^ Z.of_nat k) + Zdigit n (Z.of_nat k) * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Z.rem n (beta ^ Z.of_nat k) + Z.rem (n ÷ beta ^ Z.of_nat k) beta * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Z.rem n (beta ^ Z.of_nat k) + Z.rem n (beta ^ Z.of_nat k * beta) ÷ beta ^ Z.of_nat k * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Z.rem (Z.rem n (beta * beta ^ Z.of_nat k)) (beta ^ Z.of_nat k) + Z.rem n (beta ^ Z.of_nat k * beta) ÷ beta ^ Z.of_nat k * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Z.rem (Z.rem n (beta ^ Z.of_nat k * beta)) (beta ^ Z.of_nat k) + Z.rem n (beta ^ Z.of_nat k * beta) ÷ beta ^ Z.of_nat k * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(Z.rem (Z.rem n (beta ^ Z.of_nat (S k))) (beta ^ Z.of_nat k) + Z.rem n (beta ^ Z.of_nat (S k)) ÷ beta ^ Z.of_nat k * beta ^ Z.of_nat k)%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
(beta ^ Z.of_nat (S k))%Z = (beta ^ Z.of_nat k * beta)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(beta ^ Z.of_nat k * (Z.rem n (beta ^ Z.of_nat (S k)) ÷ beta ^ Z.of_nat k) + Z.rem (Z.rem n (beta ^ Z.of_nat (S k))) (beta ^ Z.of_nat k))%Z = Z.rem n (beta ^ Z.of_nat (S k))
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
(beta ^ Z.of_nat (S k))%Z = (beta ^ Z.of_nat k * beta)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

Z.rem n (beta ^ Z.of_nat (S k)) = (beta ^ Z.of_nat k * (Z.rem n (beta ^ Z.of_nat (S k)) ÷ beta ^ Z.of_nat k) + Z.rem (Z.rem n (beta ^ Z.of_nat (S k))) (beta ^ Z.of_nat k))%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
(beta ^ Z.of_nat (S k))%Z = (beta ^ Z.of_nat k * beta)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(beta ^ Z.of_nat (S k))%Z = (beta ^ Z.of_nat k * beta)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(beta ^ Z.succ (Z.of_nat k))%Z = (beta ^ Z.of_nat k * beta)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(beta ^ Z.succ (Z.of_nat k))%Z = (beta ^ Z.of_nat k * (beta * 1))%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(0 <= Z.of_nat k)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)
(0 <= 1)%Z
beta:radix
n:Z
k:nat
IHk:Zsum_digit (Zdigit n) k = Z.rem n (beta ^ Z.of_nat k)

(0 <= 1)%Z
easy. Qed.
beta:radix

forall n1 n2 : Z, (forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k) -> n1 = n2
beta:radix

forall n1 n2 : Z, (forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k) -> n1 = n2
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

n1 = n2
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Z.rem n1 (beta ^ Z.max (Z.abs n1) (Z.abs n2)) = n2
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Z.rem n1 (beta ^ Z.max (Z.abs n1) (Z.abs n2)) = Z.rem n2 (beta ^ Z.max (Z.abs n1) (Z.abs n2))
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Z.rem n1 (beta ^ Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))) = Z.rem n2 (beta ^ Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))))
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Zsum_digit (Zdigit n1) (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Zsum_digit (Zdigit n2) (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Zsum_digit (Zdigit n1) 0 = Zsum_digit (Zdigit n2) 0
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
n:nat
IHn:Zsum_digit (Zdigit n1) n = Zsum_digit (Zdigit n2) n
Zsum_digit (Zdigit n1) (S n) = Zsum_digit (Zdigit n2) (S n)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
n:nat
IHn:Zsum_digit (Zdigit n1) n = Zsum_digit (Zdigit n2) n

Zsum_digit (Zdigit n1) (S n) = Zsum_digit (Zdigit n2) (S n)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
n:nat
IHn:Zsum_digit (Zdigit n1) n = Zsum_digit (Zdigit n2) n

(Zsum_digit (Zdigit n1) n + Zdigit n1 (Z.of_nat n) * beta ^ Z.of_nat n)%Z = (Zsum_digit (Zdigit n2) n + Zdigit n2 (Z.of_nat n) * beta ^ Z.of_nat n)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
n:nat
IHn:Zsum_digit (Zdigit n1) n = Zsum_digit (Zdigit n2) n

(Zsum_digit (Zdigit n2) n + Zdigit n2 (Z.of_nat n) * beta ^ Z.of_nat n)%Z = (Zsum_digit (Zdigit n2) n + Zdigit n2 (Z.of_nat n) * beta ^ Z.of_nat n)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
n:nat
IHn:Zsum_digit (Zdigit n1) n = Zsum_digit (Zdigit n2) n
(0 <= Z.of_nat n)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
n:nat
IHn:Zsum_digit (Zdigit n1) n = Zsum_digit (Zdigit n2) n

(0 <= Z.of_nat n)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

Z.abs (Z.max (Z.abs n1) (Z.abs n2)) = Z.max (Z.abs n1) (Z.abs n2)
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(0 <= Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(0 <= Z.abs n1)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 <= Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n1 <= Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n2 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n2 < beta ^ Z.abs n2)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(beta ^ Z.abs n2 <= beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(beta ^ Z.abs n2 <= beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n2 <= Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n1 < beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n1 < beta ^ Z.abs n1)%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k
(beta ^ Z.abs n1 <= beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(beta ^ Z.abs n1 <= beta ^ Z.max (Z.abs n1) (Z.abs n2))%Z
beta:radix
n1, n2:Z
H:forall k : Z, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k

(Z.abs n1 <= Z.max (Z.abs n1) (Z.abs n2))%Z
apply Z.le_max_l. Qed.
beta:radix

forall u v n : Z, (0 <= u * v)%Z -> (forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z) -> Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix

forall u v n : Z, (0 <= u * v)%Z -> (forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z) -> Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z

Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

Z.rem (Z.rem u (beta ^ n) + Z.rem v (beta ^ n)) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.abs (Z.rem u (beta ^ n) + Z.rem v (beta ^ n)) < beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(n <= n)%Z -> (Z.abs (Z.rem u (beta ^ n) + Z.rem v (beta ^ n)) < beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.abs n <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.abs n) + Z.rem v (beta ^ Z.abs n)) < beta ^ Z.abs n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.of_nat (Z.abs_nat n) <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat (Z.abs_nat n)) + Z.rem v (beta ^ Z.of_nat (Z.abs_nat n))) < beta ^ Z.of_nat (Z.abs_nat n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.of_nat 0 <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat 0) + Z.rem v (beta ^ Z.of_nat 0)) < beta ^ Z.of_nat 0)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
(Z.of_nat (S p) <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat (S p)) + Z.rem v (beta ^ Z.of_nat (S p))) < beta ^ Z.of_nat (S p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z

(Z.of_nat (S p) <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat (S p)) + Z.rem v (beta ^ Z.of_nat (S p))) < beta ^ Z.of_nat (S p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z

(Z.of_nat (S p) <= n)%Z -> (Z.abs (Zsum_digit (Zdigit u) (S p) + Zsum_digit (Zdigit v) (S p)) < beta ^ Z.of_nat (S p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z

(Z.of_nat (S p) <= n)%Z -> (Z.abs (Zsum_digit (Zdigit u) p + Zdigit u (Z.of_nat p) * beta ^ Z.of_nat p + (Zsum_digit (Zdigit v) p + Zdigit v (Z.of_nat p) * beta ^ Z.of_nat p)) < beta ^ Z.of_nat (S p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z

(Z.succ (Z.of_nat p) <= n)%Z -> (Z.abs (Zsum_digit (Zdigit u) p + Zdigit u (Z.of_nat p) * beta ^ Z.of_nat p + (Zsum_digit (Zdigit v) p + Zdigit v (Z.of_nat p) * beta ^ Z.of_nat p)) < beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zsum_digit (Zdigit u) p + Zdigit u (Z.of_nat p) * beta ^ Z.of_nat p + (Zsum_digit (Zdigit v) p + Zdigit v (Z.of_nat p) * beta ^ Z.of_nat p)) < beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zsum_digit (Zdigit u) p + Zsum_digit (Zdigit v) p + (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) < beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zsum_digit (Zdigit u) p + Zsum_digit (Zdigit v) p) + Z.abs ((Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) < beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zsum_digit (Zdigit u) p + Zsum_digit (Zdigit v) p) + Z.abs ((Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) < beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zsum_digit (Zdigit u) p + Zsum_digit (Zdigit v) p) < beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(Z.abs ((Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) <= (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(Z.abs ((Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) <= (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.of_nat p <= n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(Z.abs ((Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) <= (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs ((Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p) <= (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * Z.abs (beta ^ Z.of_nat p) <= (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) * beta ^ Z.of_nat p <= (beta - 1) * beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) <= beta - 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(0 <= beta ^ Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) <= beta - 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z

(Z.abs (Zdigit n k) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z

(0 < beta)%Z
beta:radix
n, k:Z
H:(0 < beta)%Z
(Z.abs (Zdigit n k) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z

(0 < 2)%Z
beta:radix
n, k:Z
(2 <= beta)%Z
beta:radix
n, k:Z
H:(0 < beta)%Z
(Z.abs (Zdigit n k) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z

(2 <= beta)%Z
beta:radix
n, k:Z
H:(0 < beta)%Z
(Z.abs (Zdigit n k) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z

(2 <=? beta)%Z = true
beta:radix
n, k:Z
H:(0 < beta)%Z
(Z.abs (Zdigit n k) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z
H:(0 < beta)%Z

(Z.abs (Zdigit n k) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z
H:(0 < beta)%Z

(Z.abs (Zdigit n k) < Z.abs beta)%Z
beta:radix
n, k:Z
H:(0 < beta)%Z
Z.abs beta = Z.succ (beta - 1)
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z
H:(0 < beta)%Z

beta <> 0%Z
beta:radix
n, k:Z
H:(0 < beta)%Z
Z.abs beta = Z.succ (beta - 1)
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z
H:(0 < beta)%Z

Z.abs beta = Z.succ (beta - 1)
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z
H:(0 < beta)%Z

beta = Z.succ (beta - 1)
beta:radix
n, k:Z
H:(0 < beta)%Z
(0 <= beta)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
n, k:Z
H:(0 < beta)%Z

(0 <= beta)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z

(0 <= Z.of_nat p < n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z

(0 <= Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
(Z.of_nat p < n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z

(Z.of_nat p < n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z

(n > Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z

(Z.abs (Zdigit u (Z.of_nat p) + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
K:Zdigit u (Z.of_nat p) = 0%Z

(Z.abs (0 + Zdigit v (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
K:Zdigit v (Z.of_nat p) = 0%Z
(Z.abs (Zdigit u (Z.of_nat p) + 0) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
K:Zdigit v (Z.of_nat p) = 0%Z

(Z.abs (Zdigit u (Z.of_nat p) + 0) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
H:forall u0 v0 : Z, (Z.abs (Zdigit u0 v0) < Z.succ (beta - 1))%Z
H0:(0 <= Z.of_nat p < n)%Z
K:Zdigit v (Z.of_nat p) = 0%Z

(Z.abs (Zdigit u (Z.of_nat p)) < Z.succ (beta - 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ Z.succ (Z.of_nat p))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(beta ^ Z.of_nat p + (beta - 1) * beta ^ Z.of_nat p)%Z = (beta ^ (Z.of_nat p + 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(beta ^ Z.of_nat p * beta)%Z = (beta ^ (Z.of_nat p + 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(beta ^ Z.of_nat p * beta)%Z = (beta ^ Z.of_nat p * beta ^ 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(0 <= Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(0 <= 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(beta ^ Z.of_nat p * beta)%Z = (beta ^ Z.of_nat p * (beta * 1))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(0 <= Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(0 <= 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(0 <= Z.of_nat p)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z
(0 <= 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
p:nat
IHp:(Z.of_nat p <= n)%Z -> (Z.abs (Z.rem u (beta ^ Z.of_nat p) + Z.rem v (beta ^ Z.of_nat p)) < beta ^ Z.of_nat p)%Z
Hn':(Z.succ (Z.of_nat p) <= n)%Z

(0 <= 1)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z

Z.rem (u + v) (beta ^ n) = (Z.rem u (beta ^ n) + Z.rem v (beta ^ n))%Z
beta:radix
u, v:Z
n:positive
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < Z.neg n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(Z.neg n < 0)%Z

Z.rem (u + v) (beta ^ Z.neg n) = (Z.rem u (beta ^ Z.neg n) + Z.rem v (beta ^ Z.neg n))%Z
now rewrite 3!Zrem_0_r. Qed.
beta:radix

forall u v n : Z, (0 <= u * v)%Z -> (forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z) -> ((u + v) ÷ beta ^ n)%Z = (u ÷ beta ^ n + v ÷ beta ^ n)%Z
beta:radix

forall u v n : Z, (0 <= u * v)%Z -> (forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z) -> ((u + v) ÷ beta ^ n)%Z = (u ÷ beta ^ n + v ÷ beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z

((u + v) ÷ beta ^ n)%Z = (u ÷ beta ^ n + v ÷ beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z

((u + v) ÷ beta ^ n)%Z = (u ÷ beta ^ n + v ÷ beta ^ n + 0)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z

(u ÷ beta ^ n + v ÷ beta ^ n + (Z.rem u (beta ^ n) + Z.rem v (beta ^ n)) ÷ beta ^ n)%Z = (u ÷ beta ^ n + v ÷ beta ^ n + 0)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z

(u ÷ beta ^ n + v ÷ beta ^ n + Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = (u ÷ beta ^ n + v ÷ beta ^ n + 0)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z

(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.abs (Z.rem (u + v) (beta ^ n)) < beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(Z.abs (Z.rem (u + v) (beta ^ n)) < Z.abs (beta ^ n))%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
(0 <= beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(beta ^ n)%Z <> 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
(0 <= beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(0 < beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z
(0 <= beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(0 <= n)%Z

(0 <= beta ^ n)%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z
(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Huv:(0 <= u * v)%Z
Hd:forall k : Z, (0 <= k < n)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z
Hn:(n < 0)%Z

(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v, n:Z
Hn:(n < 0)%Z

(Z.rem (u + v) (beta ^ n) ÷ beta ^ n)%Z = 0%Z
beta:radix
u, v:Z
n:positive
Hn:(Z.neg n < 0)%Z

(Z.rem (u + v) (beta ^ Z.neg n) ÷ beta ^ Z.neg n)%Z = 0%Z
apply Zquot_0_r. Qed.
beta:radix

forall u v : Z, (0 <= u * v)%Z -> (forall k : Z, (0 <= k)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z) -> forall k : Z, Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix

forall u v : Z, (0 <= u * v)%Z -> (forall k : Z, (0 <= k)%Z -> Zdigit u k = 0%Z \/ Zdigit v k = 0%Z) -> forall k : Z, Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z

Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

Z.rem ((u + v) ÷ beta ^ k) beta = (Z.rem (u ÷ beta ^ k) beta + Z.rem (v ÷ beta ^ k) beta)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

Z.rem (u ÷ beta ^ k + v ÷ beta ^ k) beta = (Z.rem (u ÷ beta ^ k) beta + Z.rem (v ÷ beta ^ k) beta)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

Z.rem (u ÷ beta ^ k + v ÷ beta ^ k) (beta * 1) = (Z.rem (u ÷ beta ^ k) (beta * 1) + Z.rem (v ÷ beta ^ k) (beta * 1))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

Z.rem (u ÷ beta ^ k + v ÷ beta ^ k) (beta ^ 1) = (Z.rem (u ÷ beta ^ k) (beta ^ 1) + Z.rem (v ÷ beta ^ k) (beta ^ 1))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= u ÷ beta ^ k * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

v = 0%Z -> (v ÷ beta ^ k)%Z = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= u ÷ beta ^ k * v)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
Zv:v = 0%Z

(0 ÷ beta ^ k)%Z = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= u ÷ beta ^ k * v)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= u ÷ beta ^ k * v)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= v * (u ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

u = 0%Z -> (u ÷ beta ^ k)%Z = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * u)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= u * (u ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
Zu:u = 0%Z

(0 ÷ beta ^ k)%Z = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * u)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= u * (u ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= v * u)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= u * (u ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= u * (u ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= beta ^ k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= v * (v ÷ beta ^ k))%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

(0 <= beta ^ k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

forall k0 : Z, (0 <= k0 < 1)%Z -> Zdigit (u ÷ beta ^ k) k0 = 0%Z \/ Zdigit (v ÷ beta ^ k) k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
k':Z
Hk1:(0 <= k')%Z
Hk2:(k' < 1)%Z

Zdigit (u ÷ beta ^ k) k' = 0%Z \/ Zdigit (v ÷ beta ^ k) k' = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
k':Z
Hk1:(0 <= k')%Z
Hk2:(k' < 1)%Z

Zdigit u (k' + k) = 0%Z \/ Zdigit v (k' + k) = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
k':Z
Hk1:(0 <= k')%Z
Hk2:(k' < 1)%Z

(0 <= k' + k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z

forall k0 : Z, (0 <= k0 < k)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(0 <= k)%Z
k':Z
Hk1:(0 <= k')%Z
Hk2:(k' < k)%Z

Zdigit u k' = 0%Z \/ Zdigit v k' = 0%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
beta:radix
u, v:Z
Huv:(0 <= u * v)%Z
Hd:forall k0 : Z, (0 <= k0)%Z -> Zdigit u k0 = 0%Z \/ Zdigit v k0 = 0%Z
k:Z
Hk:(k < 0)%Z

Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z
now rewrite 3!Zdigit_lt. Qed.
Left and right shifts
Definition Zscale n k :=
  if Zle_bool 0 k then (n * Zpower beta k)%Z else Z.quot n (Zpower beta (-k)).

beta:radix

forall n k k' : Z, (0 <= k')%Z -> Zdigit (Zscale n k) k' = Zdigit n (k' - k)
beta:radix

forall n k k' : Z, (0 <= k')%Z -> Zdigit (Zscale n k) k' = Zdigit n (k' - k)