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

Copyright (C) 2011-2013 Sylvie Boldo
#<br />#
Copyright (C) 2011-2013 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.
*)

Require Import ZArith.
Require Import Zquot.
Require Import Fcore_Zaux.

(** 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.

Theorem digits2_Pnat_correct :
  forall n,
  let d := digits2_Pnat n in
  (Zpower_nat 2 d <= Zpos n < Zpower_nat 2 (S d))%Z.
Proof.
(* Goal: forall n : positive, let d := digits2_Pnat n in and (Z.le (Zpower_nat (Zpos (xO xH)) d) (Zpos n)) (Z.lt (Zpos n) (Zpower_nat (Zpos (xO xH)) (S d))) *)
intros n d. unfold d. clear.
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) (digits2_Pnat n)) (Zpos n)) (Z.lt (Zpos n) (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n)))) *)
assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy.
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) (digits2_Pnat n)) (Zpos n)) (Z.lt (Zpos n) (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n)))) *)
induction n ; simpl digits2_Pnat.
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n))) (Zpos (xI n))) (Z.lt (Zpos (xI n)) (Zpower_nat (Zpos (xO xH)) (S (S (digits2_Pnat n))))) *)
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n))) (Zpos (xO n))) (Z.lt (Zpos (xO n)) (Zpower_nat (Zpos (xO xH)) (S (S (digits2_Pnat n))))) *)
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) O) (Zpos xH)) (Z.lt (Zpos xH) (Zpower_nat (Zpos (xO xH)) (S O))) *)
rewrite Zpos_xI, 2!Hp.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n))) (Zpos (xO n))) (Z.lt (Zpos (xO n)) (Zpower_nat (Zpos (xO xH)) (S (S (digits2_Pnat n))))) *)
(* Goal: and (Z.le (Zpower_nat (Zpos (xO xH)) O) (Zpos xH)) (Z.lt (Zpos xH) (Zpower_nat (Zpos (xO xH)) (S O))) *)
rewrite (Zpos_xO n), 2!Hp.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
now split.
Qed.

Section Fcore_digits.

Variable beta : radix.

Definition Zdigit n k := Z.rem (Z.quot n (Zpower beta k)) beta.

Theorem Zdigit_lt :
  forall n k,
  (k < 0)%Z ->
  Zdigit n k = Z0.
Proof.
(* Goal: forall (n k : Z) (_ : Z.lt k Z0), @eq Z (Zdigit n k) Z0 *)
intros n [|k|k] Hk ; try easy.
(* Goal: @eq Z (Zdigit n (Zneg k)) Z0 *)
now case n.
Qed.

Theorem Zdigit_0 :
  forall k, Zdigit 0 k = Z0.
Proof.
(* Goal: forall k : Z, @eq Z (Zscale Z0 k) Z0 *)
intros k.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot Z0 (Z.pow (radix_val beta) k)) (radix_val beta)) Z0 *)
rewrite Zquot_0_l.
(* Goal: @eq Z (Z.rem Z0 (Z.pow (radix_val beta) k')) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zscale n (Z.opp k))) *)
(* Goal: Z.le Z0 (Z.mul (Zscale n (Z.opp k)) (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k'))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zrem_0_l.
Qed.

Theorem Zdigit_opp :
  forall n k,
  Zdigit (-n) k = Zopp (Zdigit n k).
Proof.
(* Goal: forall n k : Z, Z.le Z0 (Z.mul n (Zscale n k)) *)
intros n k.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.opp n) (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.opp (Z.rem (Z.quot n (Z.pow (radix_val beta) k)) (radix_val beta))) *)
rewrite Zquot_opp_l.
(* Goal: @eq Z (Z.rem (Z.opp (Z.quot n (Z.pow (radix_val beta) k))) (radix_val beta)) (Z.opp (Z.rem (Z.quot n (Z.pow (radix_val beta) k)) (radix_val beta))) *)
apply Zrem_opp_l.
Qed.

Theorem Zdigit_ge_Zpower_pos :
  forall e n,
  (0 <= n < Zpower beta e)%Z ->
  forall k, (e <= k)%Z -> Zdigit n k = Z0.
Proof.
(* Goal: forall (e n : Z) (_ : and (Z.le Z0 n) (Z.lt n (Z.pow (radix_val beta) e))) (k : Z) (_ : Z.le e k), @eq Z (Zdigit n k) Z0 *)
intros e n Hn k Hk.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot n (Z.pow (radix_val beta) k)) (radix_val beta)) Z0 *)
rewrite Zquot_small.
(* Goal: @eq Z (Z.rem Z0 (Z.pow (radix_val beta) k')) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zscale n (Z.opp k))) *)
(* Goal: Z.le Z0 (Z.mul (Zscale n (Z.opp k)) (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k'))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zrem_0_l.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
split.
(* Goal: Z.le Z0 n *)
(* Goal: Z.lt n (Z.pow (radix_val beta) k) *)
apply Hn.
(* Goal: Z.lt n (Z.pow (radix_val beta) k) *)
apply Zlt_le_trans with (1 := proj2 Hn).
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) k) *)
replace k with (e + (k - e))%Z by ring.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.add e (Z.sub k e))) *)
rewrite Zpower_plus.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.mul (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.sub k e))) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
rewrite <- (Zmult_1_r (beta ^ e)) at 1.
(* Goal: Z.le (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
apply Zmult_le_compat_l.
(* Goal: Z.le (Zpos xH) (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
apply (Zlt_le_succ 0).
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
apply Zpower_gt_0.
(* Goal: Z.le Z0 (Z.sub k k') *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
now apply Zle_minus_le_0.
(* Goal: Z.le Z0 (Zdigits n) *)
apply Zlt_le_weak.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zle_lt_trans with n.
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
generalize (Zle_lt_trans _ _ _ (proj1 Hn) (proj2 Hn)).
(* Goal: forall _ : and (Z.le (Z.pow (radix_val beta) (Z.sub (Zpos xH) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Zpos xH)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
clear.
(* Goal: forall _ : Z.lt Z0 (Z.pow (radix_val beta) e), Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now destruct e as [|e|e].
(* Goal: Z.le Z0 (Z.sub k k') *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
now apply Zle_minus_le_0.
Qed.

Theorem Zdigit_ge_Zpower :
  forall e n,
  (Zabs n < Zpower beta e)%Z ->
  forall k, (e <= k)%Z -> Zdigit n k = Z0.
Proof.
(* Goal: forall (e n : Z) (_ : Z.lt (Z.abs n) (Z.pow (radix_val beta) e)) (k : Z) (_ : Z.le e k), @eq Z (Zdigit n k) Z0 *)
intros e [|n|n] Hn k.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: forall _ : Z.le e k, @eq Z (Zdigit (Zpos n) k) Z0 *)
(* Goal: forall _ : Z.le e k, @eq Z (Zdigit (Zneg n) k) Z0 *)
apply Zdigit_ge_Zpower_pos.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
now split.
(* Goal: forall _ : Z.le e k, @eq Z (Zdigit (Zneg n) k) Z0 *)
intros He.
(* Goal: @eq Z (Zdigit (Zneg n) k) Z0 *)
change (Zneg n) with (Zopp (Zpos n)).
(* Goal: @eq Z (Zdigit (Z.opp (Zpos n)) k) Z0 *)
rewrite Zdigit_opp.
(* Goal: @eq Z (Z.opp (Zdigit (Zpos n) k)) Z0 *)
rewrite Zdigit_ge_Zpower_pos with (2 := He).
(* Goal: @eq Z (Z.opp Z0) Z0 *)
(* Goal: and (Z.le Z0 (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) e)) *)
apply Zopp_0.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
now split.
Qed.

Theorem Zdigit_not_0_pos :
  forall e n, (0 <= e)%Z ->
  (Zpower beta e <= n < Zpower beta (e + 1))%Z ->
  Zdigit n e <> Z0.
Proof.
(* Goal: forall (e n : Z) (_ : Z.le Z0 e) (_ : and (Z.le (Z.pow (radix_val beta) e) n) (Z.lt n (Z.pow (radix_val beta) (Z.add e (Zpos xH))))), not (@eq Z (Zdigit n e) Z0) *)
intros e n He (Hn1,Hn2).
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.add (Z.rem n (Z.pow (radix_val beta) (Z.of_nat k))) (Z.mul (Z.rem (Z.quot n (Z.pow (radix_val beta) (Z.of_nat k))) (radix_val beta)) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
rewrite <- ZOdiv_mod_mult.
(* Goal: not (@eq Z (Z.quot (Z.rem n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta))) (Z.pow (radix_val beta) e)) Z0) *)
rewrite Zrem_small.
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
intros H.
(* Goal: False *)
(* Goal: and (Z.le Z0 n) (Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta))) *)
apply Zle_not_lt with (1 := Hn1).
(* Goal: Z.lt n (Z.pow (radix_val beta) e) *)
(* Goal: and (Z.le Z0 n) (Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta))) *)
rewrite (Z.quot_rem' n (beta ^ e)).
(* Goal: Z.lt (Z.add (Z.mul (Z.pow (radix_val beta) e) (Z.quot n (Z.pow (radix_val beta) e))) (Z.rem n (Z.pow (radix_val beta) e))) (Z.pow (radix_val beta) e) *)
(* Goal: and (Z.le Z0 n) (Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta))) *)
rewrite H, Zmult_0_r, Zplus_0_l.
(* Goal: Z.lt (Z.rem n (Z.pow (radix_val beta) e)) (Z.pow (radix_val beta) e) *)
(* Goal: and (Z.le Z0 n) (Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta))) *)
apply Zrem_lt_pos_pos.
(* Goal: Z.le Z0 n *)
(* Goal: Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta)) *)
apply Zle_trans with (2 := Hn1).
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
split.
(* Goal: Z.le Z0 n *)
(* Goal: Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta)) *)
apply Zle_trans with (2 := Hn1).
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: Z.lt n (Z.mul (Z.pow (radix_val beta) e) (radix_val beta)) *)
replace (beta ^ e * beta)%Z with (beta ^ (e + 1))%Z.
(* Goal: Z.lt n (Z.pow (radix_val beta) (Z.add e (Zpos xH))) *)
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.add e (Zpos xH))) (Z.mul (Z.pow (radix_val beta) e) (radix_val beta)) *)
exact Hn2.
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.succ (Z.of_nat k))) (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta)) *)
rewrite <- (Zmult_1_r beta) at 3.
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.add e (Zpos xH))) (Z.mul (Z.pow (radix_val beta) e) (Z.mul (radix_val beta) (Zpos xH))) *)
now apply (Zpower_plus beta e 1).
Qed.

Theorem Zdigit_not_0 :
  forall e n, (0 <= e)%Z ->
  (Zpower beta e <= Zabs n < Zpower beta (e + 1))%Z ->
  Zdigit n e <> Z0.
Proof.
(* Goal: forall (e n : Z) (_ : Z.le Z0 e) (_ : and (Z.le (Z.pow (radix_val beta) e) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Z.add e (Zpos xH))))), not (@eq Z (Zdigit n e) Z0) *)
intros e n He Hn.
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
destruct (Zle_or_lt 0 n) as [Hn'|Hn'].
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
rewrite (Zabs_eq _ Hn') in Hn.
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
now apply Zdigit_not_0_pos.
(* Goal: not (@eq Z (Zdigit n e) Z0) *)
intros H.
(* Goal: Z.le Z0 (Zdigits n) *)
rewrite (Zabs_non_eq n) in Hn by now apply Zlt_le_weak.
(* Goal: False *)
apply (Zdigit_not_0_pos _ _ He Hn).
(* Goal: @eq Z (Zdigit (Z.opp n) e) Z0 *)
now rewrite Zdigit_opp, H.
Qed.

Theorem Zdigit_mul_pow :
  forall n k k', (0 <= k')%Z ->
  Zdigit (n * Zpower beta k') k = Zdigit n (k - k').
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k'), @eq Z (Zdigit (Zscale n k) k') (Zdigit n (Z.sub k' k)) *)
intros n k k' Hk'.
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
destruct (Zle_or_lt k' k) as [H|H].
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
revert k H.
(* Goal: forall (k : Z) (_ : Z.le k' k), @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
pattern k' ; apply Zlt_0_ind with (2 := Hk').
(* Goal: forall (x : Z) (_ : forall (y : Z) (_ : and (Z.le Z0 y) (Z.lt y x)) (k : Z) (_ : Z.le y k), @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) y)) k) (Zdigit n (Z.sub k y))) (_ : Z.le Z0 x) (k : Z) (_ : Z.le x k), @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) x)) k) (Zdigit n (Z.sub k x)) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
clear k' Hk'.
(* Goal: forall (x : Z) (_ : forall (y : Z) (_ : and (Z.le Z0 y) (Z.lt y x)) (k : Z) (_ : Z.le y k), @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) y)) k) (Zdigit n (Z.sub k y))) (_ : Z.le Z0 x) (k : Z) (_ : Z.le x k), @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) x)) k) (Zdigit n (Z.sub k x)) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
intros k' IHk' Hk' k H.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.mul n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.rem (Z.quot n (Z.pow (radix_val beta) (Z.sub k k'))) (radix_val beta)) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
apply (f_equal (fun x => Z.rem x beta)).
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) k)) (Z.quot n (Z.pow (radix_val beta) (Z.sub k k'))) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
pattern k at 1 ; replace k with (k - k' + k')%Z by ring.
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) (Z.add (Z.sub k k') k'))) (Z.quot n (Z.pow (radix_val beta) (Z.sub k k'))) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
rewrite Zpower_plus with (2 := Hk').
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.mul (Z.pow (radix_val beta) (Z.opp (Z.add k k'))) (Z.pow (radix_val beta) k))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
(* Goal: Z.le Z0 (Z.opp (Z.add k k')) *)
apply Zquot_mult_cancel_r.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: Z.le Z0 (Z.sub k k') *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
now apply Zle_minus_le_0.
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
destruct (Zle_or_lt 0 k) as [H0|H0].
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite (Zdigit_lt n) by omega.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.mul n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) k)) (radix_val beta)) Z0 *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
replace k' with (k' - k + k)%Z by ring.
(* Goal: @eq Z (Z.rem (Z.quot (Z.mul n (Z.pow (radix_val beta) (Z.add (Z.sub k' k) k))) (Z.pow (radix_val beta) k)) (radix_val beta)) Z0 *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
rewrite Zpower_plus with (2 := H0).
(* Goal: @eq Z (Z.quot (Z.mul n (Z.mul (Z.pow (radix_val beta) (Z.add k k')) (Z.pow (radix_val beta) (Z.opp k')))) (Z.pow (radix_val beta) (Z.opp k'))) (Z.mul n (Z.pow (radix_val beta) (Z.add k k'))) *)
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
rewrite Zmult_assoc, Z_quot_mult.
(* Goal: @eq Z (Z.rem (Z.mul n (Z.pow (radix_val beta) (Z.sub k' k))) (radix_val beta)) Z0 *)
(* Goal: not (@eq Z (Z.pow (radix_val beta) k) Z0) *)
(* Goal: Z.le Z0 (Z.sub k' k) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite Zpower_exp by omega.
(* Goal: Z.le Z0 (Z.mul n (Z.mul n (Z.pow (radix_val beta) k))) *)
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
rewrite Zmult_assoc.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.sub k' (Z.add k (Zpos xH)))) (Z.mul (Z.pow (radix_val beta) k) (Z.pow (radix_val beta) (Zpos xH))))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
change (Zpower beta 1) with (beta * 1)%Z.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.sub k' (Z.add k (Zpos xH)))) (Z.mul (Z.pow (radix_val beta) k) (Z.mul (radix_val beta) (Zpos xH))))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
rewrite Zmult_1_r.
(* Goal: @eq Z (Z.rem (Z.mul (Z.mul n (Z.pow (radix_val beta) (Z.sub (Z.sub k' k) (Zpos xH)))) (radix_val beta)) (radix_val beta)) Z0 *)
(* Goal: not (@eq Z (Z.pow (radix_val beta) k) Z0) *)
(* Goal: Z.le Z0 (Z.sub k' k) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
apply Z_rem_mult.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: Z.le Z0 (Z.sub k' k) *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
apply Zle_minus_le_0.
(* Goal: Z.le Z0 (Zdigits n) *)
now apply Zlt_le_weak.
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
rewrite Zdigit_lt with (1 := H0).
(* Goal: @eq Z Z0 (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
apply sym_eq.
(* Goal: @eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0 *)
apply Zdigit_lt.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zdigit_div_pow :
  forall n k k', (0 <= k)%Z -> (0 <= k')%Z ->
  Zdigit (Z.quot n (Zpower beta k')) k = Zdigit n (k + k').
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k) (_ : Z.le Z0 k'), @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.add k k')) *)
intros n k k' Hk Hk'.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.quot n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.rem (Z.quot n (Z.pow (radix_val beta) (Z.add k k'))) (radix_val beta)) *)
rewrite Zquot_Zquot.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.pow (radix_val beta) (Z.add (Zpos xH) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.pow (radix_val beta) (Z.add (Zpos xH) v)) u))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
rewrite Zplus_comm.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.add e (Z.sub k e))) *)
now rewrite Zpower_plus.
Qed.

Theorem Zdigit_mod_pow :
  forall n k k', (k < k')%Z ->
  Zdigit (Z.rem n (Zpower beta k')) k = Zdigit n k.
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k), @eq Z (Zscale (Zscale n k) k') (Zscale n (Z.add k k')) *)
intros n k k' Hk.
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
destruct (Zle_or_lt 0 k) as [H|H].
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.rem n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.rem (Z.quot n (Z.pow (radix_val beta) k)) (radix_val beta)) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
rewrite <- 2!ZOdiv_mod_mult.
(* Goal: @eq Z (Z.quot (Z.rem (Z.rem n (Z.pow (radix_val beta) k')) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.pow (radix_val beta) k)) (Z.quot (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.pow (radix_val beta) k)) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
apply (f_equal (fun x => Z.quot x (beta ^ k))).
(* Goal: @eq Z (Z.rem (Z.rem n (Z.pow (radix_val beta) k')) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
replace k' with (k + 1 + (k' - (k + 1)))%Z by ring.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite Zpower_exp by omega.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zmult_comm.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
rewrite Zpower_plus by easy.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.sub k' (Z.add k (Zpos xH)))) (Z.mul (Z.pow (radix_val beta) k) (Z.pow (radix_val beta) (Zpos xH))))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
change (Zpower beta 1) with (beta * 1)%Z.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.sub k' (Z.add k (Zpos xH)))) (Z.mul (Z.pow (radix_val beta) k) (Z.mul (radix_val beta) (Zpos xH))))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
rewrite Zmult_1_r.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.sub k' (Z.add k (Zpos xH)))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta)))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
apply ZOmod_mod_mult.
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) k)) (Z.add k1 k')) (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
now rewrite 2!Zdigit_lt.
Qed.

Theorem Zdigit_mod_pow_out :
  forall n k k', (0 <= k' <= k)%Z ->
  Zdigit (Z.rem n (Zpower beta k')) k = Z0.
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k), @eq Z (Zscale (Zscale n k) k') (Zscale n (Z.add k k')) *)
intros n k k' Hk.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.rem n (Z.pow (radix_val beta) k')) (Z.pow (radix_val beta) k)) (radix_val beta)) Z0 *)
rewrite ZOdiv_small_abs.
(* Goal: @eq Z (Z.rem Z0 (Z.pow (radix_val beta) k')) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zscale n (Z.opp k))) *)
(* Goal: Z.le Z0 (Z.mul (Zscale n (Z.opp k)) (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k'))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zrem_0_l.
(* Goal: Z.lt (Z.abs (Z.rem n (Z.pow (radix_val beta) k'))) (Z.pow (radix_val beta) k) *)
apply Zlt_le_trans with (Zpower beta k').
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite <- (Zabs_eq (beta ^ k')) at 2 by apply Zpower_ge_0.
(* Goal: Z.lt (Z.abs (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) (Z.abs (Z.pow (radix_val beta) l)) *)
apply Zrem_lt.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: Z.le (Z.pow (radix_val beta) (Zdigits x)) (Z.pow (radix_val beta) e) *)
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.

Theorem Zsum_digit_digit :
  forall n k,
  Zsum_digit (Zdigit n) k = Z.rem n (Zpower beta (Z_of_nat k)).
Proof.
(* Goal: forall n : Z, Z.le Z0 (Zdigits n) *)
intros n.
(* Goal: forall k : nat, @eq Z (Zsum_digit (Zdigit n) k) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat k))) *)
induction k.
(* Goal: @eq Z Z0 (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
apply sym_eq.
(* Goal: @eq Z (Z.rem n (Z.pow (radix_val beta) (Z.of_nat O))) (Zsum_digit (Zdigit n) O) *)
(* Goal: @eq Z (Zsum_digit (Zdigit n) (S k)) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
apply Zrem_1_r.
(* Goal: @eq Z (Zsum_digit (Zdigit n) (S k)) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
simpl Zsum_digit.
(* Goal: @eq Z (Z.add (Zsum_digit (Zdigit n) k) (Z.mul (Zdigit n (Z.of_nat k)) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
rewrite IHk.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.add (Z.rem n (Z.pow (radix_val beta) (Z.of_nat k))) (Z.mul (Z.rem (Z.quot n (Z.pow (radix_val beta) (Z.of_nat k))) (radix_val beta)) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
rewrite <- ZOdiv_mod_mult.
(* Goal: @eq Z (Z.add (Z.rem n (Z.pow (radix_val beta) (Z.of_nat k))) (Z.mul (Z.quot (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta))) (Z.pow (radix_val beta) (Z.of_nat k))) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
rewrite <- (ZOmod_mod_mult n beta).
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zmult_comm.
(* Goal: @eq Z (Z.add (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta))) (Z.pow (radix_val beta) (Z.of_nat k))) (Z.mul (Z.quot (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta))) (Z.pow (radix_val beta) (Z.of_nat k))) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
replace (beta ^ Z_of_nat k * beta)%Z with (Zpower beta (Z_of_nat (S k))).
(* Goal: @eq Z (Z.add (Z.rem (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) (Z.pow (radix_val beta) (Z.of_nat k))) (Z.mul (Z.quot (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) (Z.pow (radix_val beta) (Z.of_nat k))) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.of_nat (S k))) (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta)) *)
rewrite Zplus_comm, Zmult_comm.
(* Goal: @eq Z Z0 (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
apply sym_eq.
(* Goal: @eq Z (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) (Z.add (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (Z.quot (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) (Z.pow (radix_val beta) (Z.of_nat k)))) (Z.rem (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) (Z.pow (radix_val beta) (Z.of_nat k)))) *)
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.of_nat (S k))) (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta)) *)
apply Z.quot_rem'.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.of_nat (S (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite inj_S.
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.succ (Z.of_nat k))) (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (radix_val beta)) *)
rewrite <- (Zmult_1_r beta) at 3.
(* Goal: @eq Z (Z.pow (radix_val beta) (Z.succ (Z.of_nat k))) (Z.mul (Z.pow (radix_val beta) (Z.of_nat k)) (Z.mul (radix_val beta) (Zpos xH))) *)
apply Zpower_plus.
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
Qed.

Theorem Zpower_gt_id :
  forall n, (n < Zpower beta n)%Z.
Proof.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
intros [|n|n] ; try easy.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
(* Goal: Z.lt (Zpos n) (Z.pow_pos (radix_val beta) n) *)
rewrite Zpower_pos_nat.
(* Goal: Z.lt (Zpos n) (Zpower_nat (radix_val beta) (Pos.to_nat n)) *)
rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
(* Goal: Z.lt (Z.of_nat (Pos.to_nat n)) (Zpower_nat (radix_val beta) (Pos.to_nat n)) *)
induction (nat_of_P n).
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.of_nat (S (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite inj_S.
(* Goal: Z.lt (Z.succ (Z.of_nat n0)) (Zpower_nat (radix_val beta) (S n0)) *)
change (Zpower_nat beta (S n0)) with (beta * Zpower_nat beta n0)%Z.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.succ (Z.of_nat (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
unfold Zsucc.
(* Goal: Z.lt (Z.add (Z.of_nat n0) (Zpos xH)) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
apply Zlt_le_trans with (beta * (Z_of_nat n0 + 1))%Z.
(* Goal: forall _ : and (Z.le (Z.pow (radix_val beta) (Z.sub (Zpos xH) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Zpos xH)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
clear.
(* Goal: Z.lt (Z.add (Z.of_nat n0) (Zpos xH)) (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) *)
(* Goal: Z.le (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
apply Zlt_0_minus_lt.
(* Goal: Z.lt Z0 (Z.sub (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.add (Z.of_nat n0) (Zpos xH))) *)
(* Goal: Z.le (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
replace (beta * (Z_of_nat n0 + 1) - (Z_of_nat n0 + 1))%Z with ((beta - 1) * (Z_of_nat n0 + 1))%Z by ring.
(* Goal: Z.lt Z0 (Z.mul (Z.sub (radix_val beta) (Zpos xH)) (Z.add (Z.of_nat n0) (Zpos xH))) *)
(* Goal: Z.le (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
apply Zmult_lt_0_compat.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
cut (2 <= beta)%Z. omega.
(* Goal: Z.le (Zpos (xO xH)) (radix_val beta) *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_bool_imp_le.
(* Goal: @eq bool (Z.leb (Zpos (xO xH)) (radix_val beta)) true *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply beta.
(* Goal: Z.lt Z0 (Z.add (Z.of_nat n0) (Zpos xH)) *)
(* Goal: Z.le (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
apply (Zle_lt_succ 0).
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
(* Goal: Z.le (Z.mul (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH))) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
apply Zmult_le_compat_l.
(* Goal: Z.le (Z.add (Z.of_nat n0) (Zpos xH)) (Zpower_nat (radix_val beta) n0) *)
(* Goal: Z.le Z0 (radix_val beta) *)
now apply Zlt_le_succ.
(* Goal: Z.le Z0 (radix_val beta) *)
apply Zle_trans with 2%Z.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: Z.le (Zpos (xO xH)) (radix_val beta) *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_bool_imp_le.
(* Goal: @eq bool (Z.leb (Zpos (xO xH)) (radix_val beta)) true *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply beta.
Qed.

Theorem Zdigit_ext :
  forall n1 n2,
  (forall k, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k) ->
  n1 = n2.
Proof.
(* Goal: forall (n1 n2 : Z) (_ : forall (k : Z) (_ : Z.le Z0 k), @eq Z (Zdigit n1 k) (Zdigit n2 k)), @eq Z n1 n2 *)
intros n1 n2 H.
(* Goal: @eq Z n1 n2 *)
rewrite <- (ZOmod_small_abs n1 (Zpower beta (Zmax (Zabs n1) (Zabs n2)))).
(* Goal: @eq Z (Z.rem n1 (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2)))) n2 *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
rewrite <- (ZOmod_small_abs n2 (Zpower beta (Zmax (Zabs n1) (Zabs n2)))) at 2.
(* Goal: @eq Z (Z.rem n1 (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2)))) (Z.rem n2 (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2)))) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
replace (Zmax (Zabs n1) (Zabs n2)) with (Z_of_nat (Zabs_nat (Zmax (Zabs n1) (Zabs n2)))).
(* Goal: @eq Z (Z.rem n1 (Z.pow (radix_val beta) (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))))) (Z.rem n2 (Z.pow (radix_val beta) (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))))) *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
rewrite <- 2!Zsum_digit_digit.
(* Goal: @eq Z (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)))) *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
induction (Zabs_nat (Zmax (Zabs n1) (Zabs n2))).
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
(* Goal: @eq Z (Z.add (Zsum_digit (Zdigit n1) n) (Z.mul (Zdigit n1 (Z.of_nat n)) (Z.pow (radix_val beta) (Z.of_nat n)))) (Z.add (Zsum_digit (Zdigit n2) n) (Z.mul (Zdigit n2 (Z.of_nat n)) (Z.pow (radix_val beta) (Z.of_nat n)))) *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
rewrite H, IHn.
(* Goal: @eq Z Z0 Z0 *)
apply refl_equal.
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
(* Goal: @eq Z (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
rewrite inj_Zabs_nat.
(* Goal: @eq Z (Z.abs (Z.max (Z.abs n1) (Z.abs n2))) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zabs_eq.
(* Goal: Z.le Z0 (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zle_trans with (Zabs n1).
(* Goal: Z.le Z0 (Z.abs (Z.mul x y)) *)
(* Goal: Z.le (Z.abs (Z.mul x y)) (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y))) *)
(* Goal: Z.le (Zdigits (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y)))) (Z.add (Zdigits (Z.abs x)) (Zdigits (Z.abs y))) *)
apply Zabs_pos.
(* Goal: Z.le (Z.abs n1) (Z.max (Z.abs n1) (Z.abs n2)) *)
apply Zle_max_l.
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zlt_le_trans with (Zpower beta (Zabs n2)).
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.abs n1)) *)
(* Goal: Z.le (Z.pow (radix_val beta) (Z.abs n1)) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zpower_gt_id.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
apply Zpower_le.
(* Goal: Z.le (Z.abs n2) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zle_max_r.
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zlt_le_trans with (Zpower beta (Zabs n1)).
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.abs n1)) *)
(* Goal: Z.le (Z.pow (radix_val beta) (Z.abs n1)) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
apply Zpower_gt_id.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
apply Zpower_le.
(* Goal: Z.le (Z.abs n1) (Z.max (Z.abs n1) (Z.abs n2)) *)
apply Zle_max_l.
Qed.

Theorem ZOmod_plus_pow_digit :
  forall u v n, (0 <= u * v)%Z ->
  (forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
  Z.rem (u + v) (Zpower beta n) = (Z.rem u (Zpower beta n) + Z.rem v (Zpower beta n))%Z.
Proof.
(* Goal: forall (u v n : Z) (_ : Z.le Z0 (Z.mul u v)) (_ : forall (k : Z) (_ : and (Z.le Z0 k) (Z.lt k n)), or (@eq Z (Zdigit u k) Z0) (@eq Z (Zdigit v k) Z0)), @eq Z (Z.quot (Z.add u v) (Z.pow (radix_val beta) n)) (Z.add (Z.quot u (Z.pow (radix_val beta) n)) (Z.quot v (Z.pow (radix_val beta) n))) *)
intros u v n Huv Hd.
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) n)) (Z.pow (radix_val beta) n)) Z0 *)
destruct (Zle_or_lt 0 n) as [Hn|Hn].
rewrite Zplus_rem with (1 := Huv).
apply ZOmod_small_abs.
generalize (Zle_refl n).
pattern n at -2 ; rewrite <- Zabs_eq with (1 := Hn).
rewrite <- (inj_Zabs_nat n).
induction (Zabs_nat n) as [|p IHp].
now rewrite 2!Zrem_1_r.
(* Goal: @eq Z (Z.rem n1 (Z.pow (radix_val beta) (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))))) (Z.rem n2 (Z.pow (radix_val beta) (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))))) *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))) (Z.max (Z.abs n1) (Z.abs n2)) *)
(* Goal: Z.lt (Z.abs n2) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
(* Goal: Z.lt (Z.abs n1) (Z.pow (radix_val beta) (Z.max (Z.abs n1) (Z.abs n2))) *)
rewrite <- 2!Zsum_digit_digit.
(* Goal: @eq Z (Zsum_digit (Zdigit n) (S k)) (Z.rem n (Z.pow (radix_val beta) (Z.of_nat (S k)))) *)
simpl Zsum_digit.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.of_nat (S (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite inj_S.
intros Hn'.
replace (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))%Z with
  (Zsum_digit (Zdigit u) p + Zsum_digit (Zdigit v) p +
(* Goal: @eq Z (Z.add (Z.add k1 l1) (Z.sub k l1)) (Z.add k1 k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
  (Zdigit u (Z_of_nat p) + Zdigit v (Z_of_nat p)) * beta ^ Z_of_nat p)%Z by ring.
apply (Zle_lt_trans _ _ _ (Zabs_triangle _ _)).
replace (beta ^ Zsucc (Z_of_nat p))%Z with (beta ^ Z_of_nat p + (beta - 1) * beta ^ Z_of_nat p)%Z.
apply Zplus_lt_le_compat.
rewrite 2!Zsum_digit_digit.
apply IHp.
now apply Zle_succ_le.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits x) (Zpos xH)) (Z.sub (Zdigits y) (Zpos xH)))) (Z.abs (Z.mul x y)) *)
rewrite Zabs_Zmult.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite (Zabs_eq (beta ^ Z_of_nat p)) by apply Zpower_ge_0.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zmult_le_compat_r. 2: apply Zpower_ge_0.
apply Zlt_succ_le.
assert (forall u v, Zabs (Zdigit u v) < Zsucc (beta -  1))%Z.
(* Goal: forall n k : Z, Z.le Z0 (Z.mul n (Zscale n k)) *)
clear ; intros n k.
assert (0 < beta)%Z.
apply Zlt_le_trans with 2%Z.
(* Goal: @eq Z Z0 Z0 *)
apply refl_equal.
(* Goal: Z.le (Zpos (xO xH)) (radix_val beta) *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_bool_imp_le.
(* Goal: @eq bool (Z.leb (Zpos (xO xH)) (radix_val beta)) true *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply beta.
replace (Zsucc (beta - 1)) with (Zabs beta).
(* Goal: Z.lt (Z.abs (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) (Z.abs (Z.pow (radix_val beta) l)) *)
apply Zrem_lt.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
now apply Zgt_not_eq.
(* Goal: Z.lt (Z.abs (Z.add (Z.add x y) (Z.mul x y))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
rewrite Zabs_eq.
apply Zsucc_pred.
(* Goal: Z.le Z0 (Zdigits n) *)
now apply Zlt_le_weak.
assert (0 <= Z_of_nat p < n)%Z.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
split.
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
apply Zgt_lt.
now apply Zle_succ_gt.
destruct (Hd (Z_of_nat p) H0) as [K|K] ; rewrite K.
apply H.
rewrite Zplus_0_r.
apply H.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.succ (Z.of_nat (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
unfold Zsucc.
(* Goal: Z.lt (Z.add (Z.add x y) (Z.mul x y)) (Z.mul (Z.add x (Zpos xH)) (Z.add y (Zpos xH))) *)
(* Goal: Z.le (Z.mul (Z.add x (Zpos xH)) (Z.add y (Zpos xH))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
ring_simplify.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.add e (Z.sub k e))) *)
rewrite Zpower_plus.
change (beta ^1)%Z with (beta * 1)%Z.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul (Z.pow (radix_val beta) (Z.sub k' (Z.add k (Zpos xH)))) (Z.mul (Z.pow (radix_val beta) k) (Z.mul (radix_val beta) (Zpos xH))))) (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) (Z.rem n (Z.mul (Z.pow (radix_val beta) k) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.rem n (Z.pow (radix_val beta) k')) k) (Zdigit n k) *)
now rewrite Zmult_1_r.
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
destruct n as [|n|n] ; try easy.
now rewrite 3!Zrem_0_r.
Qed.

Theorem ZOdiv_plus_pow_digit :
  forall u v n, (0 <= u * v)%Z ->
  (forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
  Z.quot (u + v) (Zpower beta n) = (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))%Z.
Proof.
(* Goal: forall (u v n : Z) (_ : Z.le Z0 (Z.mul u v)) (_ : forall (k : Z) (_ : and (Z.le Z0 k) (Z.lt k n)), or (@eq Z (Zdigit u k) Z0) (@eq Z (Zdigit v k) Z0)), @eq Z (Z.quot (Z.add u v) (Z.pow (radix_val beta) n)) (Z.add (Z.quot u (Z.pow (radix_val beta) n)) (Z.quot v (Z.pow (radix_val beta) n))) *)
intros u v n Huv Hd.
(* Goal: @eq Z (Z.quot (Z.add u v) (Z.pow (radix_val beta) n)) (Z.add (Z.quot u (Z.pow (radix_val beta) n)) (Z.quot v (Z.pow (radix_val beta) n))) *)
rewrite <- (Zplus_0_r (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))).
(* Goal: @eq Z (Z.quot (Z.add u v) (Z.pow (radix_val beta) n)) (Z.add (Z.add (Z.quot u (Z.pow (radix_val beta) n)) (Z.quot v (Z.pow (radix_val beta) n))) Z0) *)
rewrite ZOdiv_plus with (1 := Huv).
(* Goal: @eq Z (Z.add (Z.add (Z.quot u (Z.pow (radix_val beta) n)) (Z.quot v (Z.pow (radix_val beta) n))) (Z.quot (Z.add (Z.rem u (Z.pow (radix_val beta) n)) (Z.rem v (Z.pow (radix_val beta) n))) (Z.pow (radix_val beta) n))) (Z.add (Z.add (Z.quot u (Z.pow (radix_val beta) n)) (Z.quot v (Z.pow (radix_val beta) n))) Z0) *)
rewrite <- ZOmod_plus_pow_digit by assumption.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Zpos (Pos.of_succ_nat (digits2_Pnat m))) *)
apply f_equal.
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) n)) (Z.pow (radix_val beta) n)) Z0 *)
destruct (Zle_or_lt 0 n) as [Hn|Hn].
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) n)) (Z.pow (radix_val beta) n)) Z0 *)
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) n)) (Z.pow (radix_val beta) n)) Z0 *)
apply ZOdiv_small_abs.
(* Goal: Z.lt (Z.abs (Z.rem (Z.add u v) (Z.pow (radix_val beta) n))) (Z.pow (radix_val beta) n) *)
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) n)) (Z.pow (radix_val beta) n)) Z0 *)
rewrite <- Zabs_eq.
(* Goal: Z.lt (Z.abs (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) (Z.abs (Z.pow (radix_val beta) l)) *)
apply Zrem_lt.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) n)) (Z.pow (radix_val beta) n)) Z0 *)
clear -Hn.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
destruct n as [|n|n] ; try easy.
(* Goal: @eq Z (Z.quot (Z.rem (Z.add u v) (Z.pow (radix_val beta) (Zneg n))) (Z.pow (radix_val beta) (Zneg n))) Z0 *)
apply Zquot_0_r.
Qed.

Theorem Zdigit_plus :
  forall u v, (0 <= u * v)%Z ->
  (forall k, (0 <= k)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
  forall k,
  Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z.
Proof.
(* Goal: forall (u v : Z) (_ : Z.le Z0 (Z.mul u v)) (_ : forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit u k) Z0) (@eq Z (Zdigit v k) Z0)) (k : Z), @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
intros u v Huv Hd k.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
destruct (Zle_or_lt 0 k) as [Hk|Hk].
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
unfold Zdigit.
(* Goal: @eq Z (Z.rem (Z.quot (Z.add u v) (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.add (Z.rem (Z.quot u (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.rem (Z.quot v (Z.pow (radix_val beta) k)) (radix_val beta))) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
rewrite ZOdiv_plus_pow_digit with (1 := Huv).
(* Goal: @eq Z (Z.rem (Z.add (Z.quot u (Z.pow (radix_val beta) k)) (Z.quot v (Z.pow (radix_val beta) k))) (radix_val beta)) (Z.add (Z.rem (Z.quot u (Z.pow (radix_val beta) k)) (radix_val beta)) (Z.rem (Z.quot v (Z.pow (radix_val beta) k)) (radix_val beta))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
rewrite <- (Zmult_1_r beta) at 3 5 7.
(* Goal: @eq Z (Z.rem (Z.add (Z.quot u (Z.pow (radix_val beta) k)) (Z.quot v (Z.pow (radix_val beta) k))) (Z.mul (radix_val beta) (Zpos xH))) (Z.add (Z.rem (Z.quot u (Z.pow (radix_val beta) k)) (Z.mul (radix_val beta) (Zpos xH))) (Z.rem (Z.quot v (Z.pow (radix_val beta) k)) (Z.mul (radix_val beta) (Zpos xH)))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
change (beta * 1)%Z with (beta ^1)%Z.
(* Goal: @eq Z (Z.rem (Z.add (Z.quot u (Z.pow (radix_val beta) k)) (Z.quot v (Z.pow (radix_val beta) k))) (Z.pow (radix_val beta) (Zpos xH))) (Z.add (Z.rem (Z.quot u (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Zpos xH))) (Z.rem (Z.quot v (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Zpos xH)))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
apply ZOmod_plus_pow_digit.
(* Goal: Z.le Z0 (Z.mul (Z.quot u (Z.pow (radix_val beta) k)) (Z.quot v (Z.pow (radix_val beta) k))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 (Zpos xH))), or (@eq Z (Zdigit (Z.quot u (Z.pow (radix_val beta) k)) k0) Z0) (@eq Z (Zdigit (Z.quot v (Z.pow (radix_val beta) k)) k0) Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
apply Zsame_sign_trans_weak with v.
(* Goal: forall _ : @eq Z v Z0, @eq Z (Z.quot v (Z.pow (radix_val beta) k)) Z0 *)
(* Goal: Z.le Z0 (Z.mul (Z.quot u (Z.pow (radix_val beta) k)) v) *)
(* Goal: Z.le Z0 (Z.mul v (Z.quot v (Z.pow (radix_val beta) k))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 (Zpos xH))), or (@eq Z (Zdigit (Z.quot u (Z.pow (radix_val beta) k)) k0) Z0) (@eq Z (Zdigit (Z.quot v (Z.pow (radix_val beta) k)) k0) Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
intros Zv ; rewrite Zv.
(* Goal: @eq Z (Z.quot Z0 (Z.pow (radix_val beta) (Z.opp k))) Z0 *)
apply Zquot_0_l.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zmult_comm.
(* Goal: Z.le Z0 (Z.mul v (Z.quot u (Z.pow (radix_val beta) k))) *)
(* Goal: Z.le Z0 (Z.mul v (Z.quot v (Z.pow (radix_val beta) k))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 (Zpos xH))), or (@eq Z (Zdigit (Z.quot u (Z.pow (radix_val beta) k)) k0) Z0) (@eq Z (Zdigit (Z.quot v (Z.pow (radix_val beta) k)) k0) Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
apply Zsame_sign_trans_weak with u.
(* Goal: forall _ : @eq Z u Z0, @eq Z (Z.quot u (Z.pow (radix_val beta) k)) Z0 *)
(* Goal: Z.le Z0 (Z.mul v u) *)
(* Goal: Z.le Z0 (Z.mul u (Z.quot u (Z.pow (radix_val beta) k))) *)
(* Goal: Z.le Z0 (Z.mul v (Z.quot v (Z.pow (radix_val beta) k))) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 (Zpos xH))), or (@eq Z (Zdigit (Z.quot u (Z.pow (radix_val beta) k)) k0) Z0) (@eq Z (Zdigit (Z.quot v (Z.pow (radix_val beta) k)) k0) Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
intros Zu ; rewrite Zu.
(* Goal: @eq Z (Z.quot Z0 (Z.pow (radix_val beta) (Z.opp k))) Z0 *)
apply Zquot_0_l.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
now rewrite Zmult_comm.
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
apply Zsame_sign_odiv.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
apply Zsame_sign_odiv.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
intros k' (Hk1,Hk2).
(* Goal: or (@eq Z (Zdigit (Z.quot u (Z.pow (radix_val beta) k)) k') Z0) (@eq Z (Zdigit (Z.quot v (Z.pow (radix_val beta) k)) k') Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
rewrite 2!Zdigit_div_pow by assumption.
(* Goal: or (@eq Z (Zdigit u (Z.add k' k)) Z0) (@eq Z (Zdigit v (Z.add k' k)) Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
apply Hd.
(* Goal: Z.le Z0 (Z.add k k') *)
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (if Z.leb Z0 (Z.add k k') then Z.mul n (Z.pow (radix_val beta) (Z.add k k')) else Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
now apply Zplus_le_0_compat.
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
intros k' (Hk1,Hk2).
(* Goal: or (@eq Z (Zdigit u (Z.add k' k)) Z0) (@eq Z (Zdigit v (Z.add k' k)) Z0) *)
(* Goal: forall (k0 : Z) (_ : and (Z.le Z0 k0) (Z.lt k0 k)), or (@eq Z (Zdigit u k0) Z0) (@eq Z (Zdigit v k0) Z0) *)
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
now apply Hd.
(* Goal: @eq Z (Zdigit (Z.add u v) k) (Z.add (Zdigit u k) (Zdigit v k)) *)
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)).

Theorem Zdigit_scale :
  forall n k k', (0 <= k')%Z ->
  Zdigit (Zscale n k) k' = Zdigit n (k' - k).
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k'), @eq Z (Zdigit (Zscale n k) k') (Zdigit n (Z.sub k' k)) *)
intros n k k' Hk'.
(* Goal: @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
unfold Zscale.
(* Goal: @eq Z (Zslice (if Z.leb Z0 k then Z.mul n (Z.pow (radix_val beta) k) else Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
case Zle_bool_spec ; intros Hk.
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k)) k') (Zdigit n (Z.sub k' k)) *)
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k') (Zdigit n (Z.sub k' k)) *)
now apply Zdigit_mul_pow.
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k') (Zdigit n (Z.sub k' k)) *)
apply Zdigit_div_pow with (1 := Hk').
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zscale_0 :
  forall k,
  Zscale 0 k = Z0.
Proof.
(* Goal: forall k : Z, @eq Z (Zscale Z0 k) Z0 *)
intros k.
(* Goal: @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
unfold Zscale.
(* Goal: Z.le Z0 (Z.mul n (if Z.leb Z0 k' then Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k') else Z0)) *)
case Zle_bool.
(* Goal: @eq Z (Z.mul Z0 (Z.pow (radix_val beta) k)) Z0 *)
(* Goal: @eq Z (Z.quot Z0 (Z.pow (radix_val beta) (Z.opp k))) Z0 *)
apply Zmult_0_l.
(* Goal: @eq Z (Z.quot Z0 (Z.pow (radix_val beta) (Z.opp k))) Z0 *)
apply Zquot_0_l.
Qed.

Theorem Zsame_sign_scale :
  forall n k,
  (0 <= n * Zscale n k)%Z.
Proof.
(* Goal: forall n k : Z, Z.le Z0 (Z.mul n (Zscale n k)) *)
intros n k.
(* Goal: @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
unfold Zscale.
(* Goal: @eq Z (Zslice (if Z.leb Z0 k then Z.mul n (Z.pow (radix_val beta) k) else Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
case Zle_bool_spec ; intros Hk.
(* Goal: Z.le Z0 (Z.mul n (Z.mul n (Z.pow (radix_val beta) k))) *)
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
rewrite Zmult_assoc.
(* Goal: Z.le Z0 (Z.mul (Z.mul n n) (Z.pow (radix_val beta) k)) *)
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
apply Zmult_le_0_compat.
(* Goal: Z.le Z0 (Zdigits n) *)
apply Zsame_sign_imp ; apply Zlt_le_weak.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
apply Zsame_sign_odiv.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
Qed.

Theorem Zscale_mul_pow :
  forall n k k', (0 <= k)%Z ->
  Zscale (n * Zpower beta k) k' = Zscale n (k + k').
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k), @eq Z (Zscale (Zscale n k) k') (Zscale n (Z.add k k')) *)
intros n k k' Hk.
(* Goal: @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
unfold Zscale.
(* Goal: @eq Z (if Z.leb Z0 k' then Z.mul (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k') else Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (if Z.leb Z0 (Z.add k k') then Z.mul n (Z.pow (radix_val beta) (Z.add k k')) else Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
case Zle_bool_spec ; intros Hk'.
(* Goal: @eq Z (Zdigit (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) k) (Zdigit n (Z.add k1 k)) *)
rewrite Zle_bool_true.
(* Goal: @eq Z (Z.mul (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k')) (Z.mul n (Z.pow (radix_val beta) (Z.add k k'))) *)
(* Goal: Z.le Z0 (Z.add k k') *)
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (if Z.leb Z0 (Z.add k k') then Z.mul n (Z.pow (radix_val beta) (Z.add k k')) else Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
rewrite <- Zmult_assoc.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Zpos (Pos.of_succ_nat (digits2_Pnat m))) *)
apply f_equal.
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.add e (Z.sub k e))) *)
now rewrite Zpower_plus.
(* Goal: Z.le Z0 (Z.add k k') *)
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (if Z.leb Z0 (Z.add k k') then Z.mul n (Z.pow (radix_val beta) (Z.add k k')) else Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
now apply Zplus_le_0_compat.
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (if Z.leb Z0 (Z.add k k') then Z.mul n (Z.pow (radix_val beta) (Z.add k k')) else Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
case Zle_bool_spec ; intros Hk''.
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (Z.mul n (Z.pow (radix_val beta) (Z.add k k'))) *)
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
pattern k at 1 ; replace k with (k + k' + -k')%Z by ring.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
assert (0 <= -k')%Z by omega.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
rewrite Zpower_plus by easy.
(* Goal: @eq Z (Z.quot (Z.mul n (Z.mul (Z.pow (radix_val beta) (Z.add k k')) (Z.pow (radix_val beta) (Z.opp k')))) (Z.pow (radix_val beta) (Z.opp k'))) (Z.mul n (Z.pow (radix_val beta) (Z.add k k'))) *)
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
rewrite Zmult_assoc, Z_quot_mult.
(* Goal: @eq Z Z0 Z0 *)
apply refl_equal.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
replace (-k')%Z with (-(k+k') + k)%Z by ring.
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.add (Z.opp (Z.add k k')) k))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
rewrite Zpower_plus with (2 := Hk).
(* Goal: @eq Z (Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.mul (Z.pow (radix_val beta) (Z.opp (Z.add k k'))) (Z.pow (radix_val beta) k))) (Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
(* Goal: Z.le Z0 (Z.opp (Z.add k k')) *)
apply Zquot_mult_cancel_r.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zscale_scale :
  forall n k k', (0 <= k)%Z ->
  Zscale (Zscale n k) k' = Zscale n (k + k').
Proof.
(* Goal: forall (n k k' : Z) (_ : Z.le Z0 k), @eq Z (Zscale (Zscale n k) k') (Zscale n (Z.add k k')) *)
intros n k k' Hk.
(* Goal: @eq Z (Zscale (Zscale n k) k') (Zscale n (Z.add k k')) *)
unfold Zscale at 2.
(* Goal: @eq Z (Zscale (if Z.leb Z0 k then Z.mul n (Z.pow (radix_val beta) k) else Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k') (Zscale n (Z.add k k')) *)
rewrite Zle_bool_true with (1 := Hk).
(* Goal: @eq Z (Zscale (Z.mul n (Z.pow (radix_val beta) k)) k') (Zscale n (Z.add k k')) *)
now apply Zscale_mul_pow.
Qed.

(** Slice of an integer *)

Definition Zslice n k1 k2 :=
  if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0.

Theorem Zdigit_slice :
  forall n k1 k2 k, (0 <= k < k2)%Z ->
  Zdigit (Zslice n k1 k2) k = Zdigit n (k1 + k).
Proof.
(* Goal: forall (n k1 k2 k : Z) (_ : Z.le k2 k), @eq Z (Zdigit (Zslice n k1 k2) k) Z0 *)
intros n k1 k2 k Hk.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: @eq Z (Zdigit (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) k) (Zdigit n (Z.add k1 k)) *)
rewrite Zle_bool_true.
(* Goal: @eq Z (Zdigit (Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2)) k) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 k2 *)
rewrite Zdigit_mod_pow by apply Hk.
(* Goal: @eq Z (Zdigit (Zscale n (Z.opp k1)) k) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 k2 *)
rewrite Zdigit_scale by apply Hk.
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.sub k' (Z.opp k1))) *)
unfold Zminus.
(* Goal: @eq Z (Zdigit n (Z.add k (Z.opp (Z.opp k1)))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 k2 *)
now rewrite Zopp_involutive, Zplus_comm.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zdigit_slice_out :
  forall n k1 k2 k, (k2 <= k)%Z ->
  Zdigit (Zslice n k1 k2) k = Z0.
Proof.
(* Goal: forall (n k1 k2 k : Z) (_ : Z.le k2 k), @eq Z (Zdigit (Zslice n k1 k2) k) Z0 *)
intros n k1 k2 k Hk.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: @eq Z (Zdigit (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) k) Z0 *)
case Zle_bool_spec ; intros Hk2.
(* Goal: @eq Z (Zdigit (Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2)) k) Z0 *)
(* Goal: @eq Z (Zdigit Z0 k) Z0 *)
apply Zdigit_mod_pow_out.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
now split.
(* Goal: @eq Z (Zdigit Z0 k) Z0 *)
apply Zdigit_0.
Qed.

Theorem Zslice_0 :
  forall k k',
  Zslice 0 k k' = Z0.
Proof.
(* Goal: forall k k' : Z, @eq Z (Zslice Z0 k k') Z0 *)
intros k k'.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: Z.le Z0 (Z.mul n (if Z.leb Z0 k' then Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k') else Z0)) *)
case Zle_bool.
(* Goal: @eq Z (Z.rem (Zscale Z0 (Z.opp k)) (Z.pow (radix_val beta) k')) Z0 *)
(* Goal: @eq Z Z0 Z0 *)
rewrite Zscale_0.
(* Goal: @eq Z (Z.rem Z0 (Z.pow (radix_val beta) k')) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zscale n (Z.opp k))) *)
(* Goal: Z.le Z0 (Z.mul (Zscale n (Z.opp k)) (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k'))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zrem_0_l.
(* Goal: @eq Z Z0 Z0 *)
apply refl_equal.
Qed.

Theorem Zsame_sign_slice :
  forall n k k',
  (0 <= n * Zslice n k k')%Z.
Proof.
(* Goal: forall n k k' : Z, Z.le Z0 (Z.mul n (Zslice n k k')) *)
intros n k k'.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: Z.le Z0 (Z.mul n (if Z.leb Z0 k' then Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k') else Z0)) *)
case Zle_bool.
(* Goal: Z.le Z0 (Z.mul n (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k'))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zsame_sign_trans_weak with (Zscale n (-k)).
(* Goal: forall _ : @eq Z (Zslice n (Z.add k1 l1) l2) Z0, @eq Z (Zscale (Zslice n (Z.add k1 l1) l2) l1) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n (Z.add k1 l1) l2)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n (Z.add k1 l1) l2) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
intros H ; rewrite H.
(* Goal: @eq Z (Z.rem Z0 (Z.pow (radix_val beta) k')) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zscale n (Z.opp k))) *)
(* Goal: Z.le Z0 (Z.mul (Zscale n (Z.opp k)) (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k'))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zrem_0_l.
(* Goal: Z.le Z0 (Z.mul (Zslice n (Z.add k1 l1) l2) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zsame_sign_scale.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zmult_comm.
(* Goal: Z.le Z0 (Z.mul (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) k')) (Zscale n (Z.opp k))) *)
(* Goal: Z.le Z0 (Z.mul n Z0) *)
apply Zrem_sgn2.
(* Goal: Z.le Z0 (Z.mul n Z0) *)
now rewrite Zmult_0_r.
Qed.

Theorem Zslice_slice :
  forall n k1 k2 k1' k2', (0 <= k1' <= k2)%Z ->
  Zslice (Zslice n k1 k2) k1' k2' = Zslice n (k1 + k1') (Zmin (k2 - k1') k2').
Proof.
(* Goal: forall (n k1 k2 k1' k2' : Z) (_ : and (Z.le Z0 k1') (Z.le k1' k2)), @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
intros n k1 k2 k1' k2' Hk1'.
(* Goal: @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
destruct (Zle_or_lt 0 k2') as [Hk2'|Hk2'].
(* Goal: @eq Z (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) (Zslice n k1 (Z.add l1 l2)) *)
apply Zdigit_ext.
(* Goal: forall (k : Z) (_ : Z.le Z0 k), @eq Z (Zdigit (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) k) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
intros k Hk.
(* Goal: @eq Z (Zdigit (Zslice (Zslice n k1 k2) k1' k2') k) (Zdigit (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) k) *)
(* Goal: @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
destruct (Zle_or_lt (Zmin (k2 - k1') k2') k) as [Hk'|Hk'].
(* Goal: @eq Z (Zdigit (Zslice (Zslice n k1 k2) k1' k2') k) (Zdigit (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) k) *)
(* Goal: @eq Z (Zdigit (Zslice (Zslice n k1 k2) k1' k2') k) (Zdigit (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) k) *)
(* Goal: @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
rewrite (Zdigit_slice_out n (k1 + k1')) with (1 := Hk').
(* Goal: @eq Z (Zdigit (Zslice (Zslice n k1 k2) k1' k2') k) Z0 *)
(* Goal: @eq Z (Zdigit (Zslice (Zslice n k1 k2) k1' k2') k) (Zdigit (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) k) *)
(* Goal: @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
destruct (Zle_or_lt k2' k) as [Hk''|Hk''].
(* Goal: @eq Z (Zdigit (Zslice n k1 l1) k) Z0 *)
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
now apply Zdigit_slice_out.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
rewrite Zdigit_slice by now split.
(* Goal: @eq Z (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) Z0 *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
apply Zdigit_slice_out.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
zify ; omega.
(* Goal: @eq Z (Zdigit (Zslice (Zslice n k1 k2) k1' k2') k) (Zdigit (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) k) *)
(* Goal: @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
rewrite Zdigit_slice by (zify ; omega).
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
rewrite (Zdigit_slice n (k1 + k1')) by now split.
(* Goal: @eq Z (Zdigit (Zslice n k1 k2) (Z.add k1' k)) (Zdigit n (Z.add (Z.add k1 k1') k)) *)
(* Goal: @eq Z (Zslice (Zslice n k1 k2) k1' k2') (Zslice n (Z.add k1 k1') (Z.min (Z.sub k2 k1') k2')) *)
rewrite Zdigit_slice.
(* Goal: Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
now rewrite Zplus_assoc.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
zify ; omega.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: @eq Z (if Z.leb Z0 k2' then Z.rem (Zscale (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) (Z.opp k1')) (Z.pow (radix_val beta) k2') else Z0) (if Z.leb Z0 (Z.min (Z.sub k2 k1') k2') then Z.rem (Zscale n (Z.opp (Z.add k1 k1'))) (Z.pow (radix_val beta) (Z.min (Z.sub k2 k1') k2')) else Z0) *)
rewrite Zmin_r.
(* Goal: @eq Z (if Z.leb Z0 k2' then Z.rem (Zscale (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) (Z.opp k1')) (Z.pow (radix_val beta) k2') else Z0) (if Z.leb Z0 k2' then Z.rem (Zscale n (Z.opp (Z.add k1 k1'))) (Z.pow (radix_val beta) k2') else Z0) *)
(* Goal: Z.le k2' (Z.sub k2 k1') *)
now rewrite Zle_bool_false.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zslice_mul_pow :
  forall n k k1 k2, (0 <= k)%Z ->
  Zslice (n * Zpower beta k) k1 k2 = Zslice n (k1 - k) k2.
Proof.
(* Goal: forall (n k k1 k2 : Z) (_ : Z.le Z0 k), @eq Z (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) (Zscale (Zslice n k (Z.add k1 k2)) (Z.opp k1)) *)
intros n k k1 k2 Hk.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: @eq Z (Zdigit (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) k) Z0 *)
case Zle_bool_spec ; intros Hk2.
(* Goal: @eq Z Z0 Z0 *)
2: apply refl_equal.
rewrite Zscale_mul_pow with (1 := Hk).
now replace (- (k1 - k))%Z with (k + -k1)%Z by ring.
Qed.

Theorem Zslice_div_pow :
  forall n k k1 k2, (0 <= k)%Z -> (0 <= k1)%Z ->
  Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zslice n (k1 + k) k2.
Proof.
intros n k k1 k2 Hk Hk1.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: @eq Z (Zdigit (if Z.leb Z0 k2 then Z.rem (Zscale n (Z.opp k1)) (Z.pow (radix_val beta) k2) else Z0) k) Z0 *)
case Zle_bool_spec ; intros Hk2.
(* Goal: @eq Z Z0 Z0 *)
2: apply refl_equal.
apply (f_equal (fun x => Z.rem x (beta ^ k2))).
(* Goal: @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
unfold Zscale.
case Zle_bool_spec ; intros Hk1'.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
replace k1 with Z0 by omega.
(* Goal: @eq Z (if Z.leb Z0 k' then Z.mul (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) k') else Z.quot (Z.mul n (Z.pow (radix_val beta) k)) (Z.pow (radix_val beta) (Z.opp k'))) (if Z.leb Z0 (Z.add k k') then Z.mul n (Z.pow (radix_val beta) (Z.add k k')) else Z.quot n (Z.pow (radix_val beta) (Z.opp (Z.add k k')))) *)
case Zle_bool_spec ; intros Hk'.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
replace k with Z0 by omega.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
now rewrite Zquot_1_r.
rewrite Zopp_involutive.
apply Zmult_1_r.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite Zle_bool_false by omega.
rewrite 2!Zopp_involutive, Zplus_comm.
rewrite Zpower_plus by assumption.
apply Zquot_Zquot.
Qed.

Theorem Zslice_scale :
  forall n k k1 k2, (0 <= k1)%Z ->
  Zslice (Zscale n k) k1 k2 = Zslice n (k1 - k) k2.
Proof.
(* Goal: forall (n k k1 k2 : Z) (_ : Z.le Z0 k1), @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
intros n k k1 k2 Hk1.
(* Goal: @eq Z (Zslice (Zscale n k) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
unfold Zscale.
(* Goal: @eq Z (Zslice (if Z.leb Z0 k then Z.mul n (Z.pow (radix_val beta) k) else Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
case Zle_bool_spec; intros Hk.
(* Goal: @eq Z (Zslice (Z.mul n (Z.pow (radix_val beta) k)) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
(* Goal: @eq Z (Zslice (Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
now apply Zslice_mul_pow.
(* Goal: @eq Z (Zslice (Z.quot n (Z.pow (radix_val beta) (Z.opp k))) k1 k2) (Zslice n (Z.sub k1 k) k2) *)
apply Zslice_div_pow with (2 := Hk1).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zslice_div_pow_scale :
  forall n k k1 k2, (0 <= k)%Z ->
  Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
Proof.
(* Goal: forall (n k k1 k2 : Z) (_ : Z.le Z0 k), @eq Z (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) (Zscale (Zslice n k (Z.add k1 k2)) (Z.opp k1)) *)
intros n k k1 k2 Hk.
(* Goal: @eq Z (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) (Zslice n k1 (Z.add l1 l2)) *)
apply Zdigit_ext.
(* Goal: forall (k0 : Z) (_ : Z.le Z0 k0), @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k0) (Zdigit (Zscale (Zslice n k (Z.add k1 k2)) (Z.opp k1)) k0) *)
intros k' Hk'.
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zscale (Zslice n k (Z.add k1 k2)) (Z.opp k1)) k') *)
rewrite Zdigit_scale with (1 := Hk').
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.sub k' (Z.opp k1))) *)
unfold Zminus.
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k' (Z.opp (Z.opp k1)))) *)
rewrite (Zplus_comm k'), Zopp_involutive.
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
destruct (Zle_or_lt k2 k') as [Hk2|Hk2].
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_slice_out with (1 := Hk2).
(* Goal: @eq Z Z0 (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
apply sym_eq.
(* Goal: @eq Z (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) Z0 *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
apply Zdigit_slice_out.
(* Goal: Z.le (Z.add k1 k2) (Z.add k1 k') *)
(* Goal: @eq Z (Zdigit (Zslice (Z.quot n (Z.pow (radix_val beta) k)) k1 k2) k') (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
now apply Zplus_le_compat_l.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
rewrite Zdigit_slice by now split.
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) k)) (Z.add k1 k')) (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
destruct (Zle_or_lt 0 (k1 + k')) as [Hk1'|Hk1'].
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite Zdigit_slice by omega.
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) k)) (Z.add k1 k')) (Zdigit n (Z.add k (Z.add k1 k'))) *)
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) k)) (Z.add k1 k')) (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
rewrite Zdigit_div_pow by assumption.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Zpos (Pos.of_succ_nat (digits2_Pnat m))) *)
apply f_equal.
(* Goal: @eq Z (Z.add (Z.add k1 l1) (Z.sub k l1)) (Z.add k1 k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
ring.
(* Goal: @eq Z (Zdigit (Z.quot n (Z.pow (radix_val beta) k)) (Z.add k1 k')) (Zdigit (Zslice n k (Z.add k1 k2)) (Z.add k1 k')) *)
now rewrite 2!Zdigit_lt.
Qed.

Theorem Zplus_slice :
  forall n k l1 l2, (0 <= l1)%Z -> (0 <= l2)%Z ->
  (Zslice n k l1 + Zscale (Zslice n (k + l1) l2) l1)%Z = Zslice n k (l1 + l2).
Proof.
(* Goal: forall (n k l1 l2 : Z) (_ : Z.le Z0 l1) (_ : Z.le Z0 l2), @eq Z (Z.add (Zslice n k l1) (Zscale (Zslice n (Z.add k l1) l2) l1)) (Zslice n k (Z.add l1 l2)) *)
intros n k1 l1 l2 Hl1 Hl2.
(* Goal: @eq Z (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) (Zslice n k1 (Z.add l1 l2)) *)
clear Hl1.
(* Goal: @eq Z (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) (Zslice n k1 (Z.add l1 l2)) *)
apply Zdigit_ext.
(* Goal: forall (k : Z) (_ : Z.le Z0 k), @eq Z (Zdigit (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) k) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
intros k Hk.
(* Goal: @eq Z (Zdigit (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) k) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
rewrite Zdigit_plus.
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_scale with (1 := Hk).
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
destruct (Zle_or_lt (l1 + l2) k) as [Hk2|Hk2].
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_slice_out with (1 := Hk2).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
now rewrite 2!Zdigit_slice_out by omega.
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_slice with (1 := conj Hk Hk2).
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
destruct (Zle_or_lt l1 k) as [Hk1|Hk1].
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_slice_out with (1 := Hk1).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite Zdigit_slice by omega.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Zpos (Pos.of_succ_nat (digits2_Pnat m))) *)
simpl ; apply f_equal.
(* Goal: @eq Z (Z.add (Z.add k1 l1) (Z.sub k l1)) (Z.add k1 k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
ring.
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_slice with (1 := conj Hk Hk1).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite (Zdigit_lt _ (k - l1)) by omega.
(* Goal: @eq Z (Z.add (Zdigit n (Z.add k1 k)) Z0) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zplus_0_r.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zmult_comm.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zsame_sign_trans_weak with n.
(* Goal: forall _ : @eq Z (Zslice n (Z.add k1 l1) l2) Z0, @eq Z (Zscale (Zslice n (Z.add k1 l1) l2) l1) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n (Z.add k1 l1) l2)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n (Z.add k1 l1) l2) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
intros H ; rewrite H.
(* Goal: @eq Z (Zslice Z0 k1 l1) Z0 *)
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zslice_0.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zmult_comm.
(* Goal: Z.le Z0 (Z.mul n (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zsame_sign_trans_weak with (Zslice n (k1 + l1) l2).
(* Goal: forall _ : @eq Z (Zslice n (Z.add k1 l1) l2) Z0, @eq Z (Zscale (Zslice n (Z.add k1 l1) l2) l1) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n (Z.add k1 l1) l2)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n (Z.add k1 l1) l2) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
intros H ; rewrite H.
(* Goal: @eq Z (Zscale Z0 l1) Z0 *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n (Z.add k1 l1) l2)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n (Z.add k1 l1) l2) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zscale_0.
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zsame_sign_slice.
(* Goal: Z.le Z0 (Z.mul (Zslice n (Z.add k1 l1) l2) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zsame_sign_scale.
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
apply Zsame_sign_slice.
(* Goal: forall (k : Z) (_ : Z.le Z0 k), @eq Z (Zdigit (Z.add (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) k) (Zdigit (Zslice n k1 (Z.add l1 l2)) k) *)
clear k Hk ; intros k Hk.
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
rewrite Zdigit_scale with (1 := Hk).
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
destruct (Zle_or_lt l1 k) as [Hk1|Hk1].
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
left.
(* Goal: @eq Z (Zdigit (Zslice n k1 l1) k) Z0 *)
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
now apply Zdigit_slice_out.
(* Goal: or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0) *)
right.
(* Goal: @eq Z (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1)) Z0 *)
apply Zdigit_lt.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Section digits_aux.

Variable p : Z.

Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
  match n with
  | O => nb
  | S n => if Zlt_bool p pow then nb else Zdigits_aux (nb + 1) (Zmult beta pow) n
  end.

End digits_aux.

(** Number of digits of an integer *)

Definition Zdigits n :=
  match n with
  | Z0 => Z0
  | Zneg p => Zdigits_aux (Zpos p) 1 beta (digits2_Pnat p)
  | Zpos p => Zdigits_aux n 1 beta (digits2_Pnat p)
  end.

Theorem Zdigits_correct :
  forall n,
  (Zpower beta (Zdigits n - 1) <= Zabs n < Zpower beta (Zdigits n))%Z.
Proof.
(* Goal: forall n : Z, and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits n) (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Zdigits n))) *)
cut (forall p, Zpower beta (Zdigits (Zpos p) - 1) <= Zpos p < Zpower beta (Zdigits (Zpos p)))%Z.
(* Goal: forall (_ : forall p : positive, and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits (Zpos p)) (Zpos xH))) (Zpos p)) (Z.lt (Zpos p) (Z.pow (radix_val beta) (Zdigits (Zpos p))))) (n : Z), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits n) (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Zdigits n))) *)
(* Goal: forall p : positive, and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits (Zpos p)) (Zpos xH))) (Zpos p)) (Z.lt (Zpos p) (Z.pow (radix_val beta) (Zdigits (Zpos p)))) *)
intros H [|n|n] ; try exact (H n).
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
now split.
(* Goal: forall n : Z, Z.le Z0 (Zdigits n) *)
intros n.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
(* *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
assert (U: (Zpos n < Zpower beta (Z_of_nat (S (digits2_Pnat n))))%Z).
(* Goal: Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.of_nat (S (digits2_Pnat n)))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zlt_le_trans with (1 := proj2 (digits2_Pnat_correct n)).
(* Goal: Z.le (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n))) (Z.pow (radix_val beta) (Z.of_nat (S (digits2_Pnat n)))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite Zpower_Zpower_nat.
(* Goal: Z.le (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n))) (Zpower_nat (radix_val beta) (Z.abs_nat (Z.of_nat (S (digits2_Pnat n))))) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite Zabs_nat_Z_of_nat.
(* Goal: Z.le (Zpower_nat (Zpos (xO xH)) (S (digits2_Pnat n))) (Zpower_nat (radix_val beta) (S (digits2_Pnat n))) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
induction (S (digits2_Pnat n)).
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: Z.le (Zpower_nat (Zpos (xO xH)) (S n0)) (Zpower_nat (radix_val beta) (S n0)) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite 2!(Zpower_nat_S).
(* Goal: Z.le (Z.mul (Zpos (xO xH)) (Zpower_nat (Zpos (xO xH)) n0)) (Z.mul (radix_val beta) (Zpower_nat (radix_val beta) n0)) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zmult_le_compat with (2 := IHn0).
(* Goal: Z.le (Zpos (xO xH)) (radix_val beta) *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_bool_imp_le.
(* Goal: @eq bool (Z.leb (Zpos (xO xH)) (radix_val beta)) true *)
(* Goal: Z.le Z0 (Zpos (xO xH)) *)
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply beta.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite <- (Zabs_nat_Z_of_nat n0).
(* Goal: Z.le Z0 (Zpower_nat (Zpos (xO xH)) (Z.abs_nat (Z.of_nat n0))) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite <- Zpower_Zpower_nat.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) (Z.of_nat n0)) *)
(* Goal: Z.le Z0 (Z.of_nat n0) *)
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply (Zpower_ge_0 (Build_radix 2 (refl_equal true))).
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
(* Goal: Z.le Z0 (Z.of_nat (S (digits2_Pnat n))) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
apply Zle_0_nat.
(* *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
revert U.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.of_nat (S (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite inj_S.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.succ (Z.of_nat (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
unfold Zsucc.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat (digits2_Pnat n)) (Zpos xH))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
generalize (digits2_Pnat n).
(* Goal: forall (n0 : nat) (_ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat n0) (Zpos xH)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) n0) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) n0))) *)
intros u U.
pattern (radix_val beta) at 2 4 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
assert (V: (Zpower beta (1 - 1) <= Zpos n)%Z).
(* Goal: Z.le (Zpos xH) (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply (Zlt_le_succ 0).
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
generalize (conj V U).
(* Goal: forall _ : and (Z.le (Z.pow (radix_val beta) (Z.sub (Zpos xH) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Zpos xH)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
clear.
(* Goal: forall _ : and (Z.le (Z.pow (radix_val beta) (Z.sub (Zpos xH) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Zpos xH)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
generalize (Zle_refl 1).
(* Goal: forall (_ : Z.le (Zpos xH) (Zpos xH)) (_ : and (Z.le (Z.pow (radix_val beta) (Z.sub (Zpos xH) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Zpos xH))))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
generalize 1%Z at 2 3 5 6 7 9 10.
(* *)
(* Goal: forall (z : Z) (_ : Z.le (Zpos xH) z) (_ : and (Z.le (Z.pow (radix_val beta) (Z.sub z (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) z)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) z (Z.pow (radix_val beta) z) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) z (Z.pow (radix_val beta) z) u))) *)
induction u.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: forall _ : Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.succ (Z.of_nat (digits2_Pnat n)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (radix_val beta) (digits2_Pnat n)))) *)
rewrite inj_S; unfold Zsucc.
(* Goal: forall (z : Z) (_ : Z.le (Zpos xH) z) (_ : and (Z.le (Z.pow (radix_val beta) (Z.sub z (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.add (Z.of_nat u) (Zpos xH)) z)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) z (Z.pow (radix_val beta) z) (S u)) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) z (Z.pow (radix_val beta) z) (S u)))) *)
simpl Zdigits_aux.
(* Goal: forall (z : Z) (_ : Z.le (Zpos xH) z) (_ : and (Z.le (Z.pow (radix_val beta) (Z.sub z (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.add (Z.of_nat u) (Zpos xH)) z)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (if Z.ltb (Zpos n) (Z.pow (radix_val beta) z) then z else Zdigits_aux (Zpos n) (Z.add z (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) z)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (if Z.ltb (Zpos n) (Z.pow (radix_val beta) z) then z else Zdigits_aux (Zpos n) (Z.add z (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) z)) u))) *)
intros v Hv U.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (if Z.ltb (Zpos n) (Z.pow (radix_val beta) v) then v else Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (if Z.ltb (Zpos n) (Z.pow (radix_val beta) v) then v else Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
case Zlt_bool_spec ; intros K.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub v (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) v)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (radix_val beta) (Z.pow (radix_val beta) v)) u))) *)
now split.
pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (Z.pow (radix_val beta) (Zpos xH)) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (Z.pow (radix_val beta) (Zpos xH)) (Z.pow (radix_val beta) v)) u))) *)
rewrite <- Zpower_plus.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.pow (radix_val beta) (Z.add (Zpos xH) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.pow (radix_val beta) (Z.add (Zpos xH) v)) u))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
rewrite Zplus_comm.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add (Zpos xH) v) (Z.pow (radix_val beta) (Z.add (Zpos xH) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add (Zpos xH) v) (Z.pow (radix_val beta) (Z.add (Zpos xH) v)) u))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
apply IHu.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
clear -Hv ; omega.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
split.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n) *)
(* Goal: Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
now ring_simplify (1 + v - 1)%Z.
(* Goal: Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
now rewrite Zplus_assoc.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: Z.le Z0 v *)
apply Zle_succ_le with (1 := Hv).
Qed.

Theorem Zdigits_unique :
  forall n d,
  (Zpower beta (d - 1) <= Zabs n < Zpower beta d)%Z ->
  Zdigits n = d.
Proof.
(* Goal: forall (n d : Z) (_ : and (Z.le (Z.pow (radix_val beta) (Z.sub d (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) d))), @eq Z (Zdigits n) d *)
intros n d Hd.
(* Goal: @eq Z (Zdigits n) d *)
assert (Hd' := Zdigits_correct n).
(* Goal: @eq Z (Zdigits n) d *)
apply Zle_antisym.
(* Goal: Z.le (Zdigits x) (Zdigits y) *)
apply (Zpower_lt_Zpower beta).
(* Goal: Z.lt (Z.pow (radix_val beta) (Z.sub d (Zpos xH))) (Z.pow (radix_val beta) (Zdigits n)) *)
now apply Zle_lt_trans with (Zabs n).
(* Goal: Z.le (Zdigits x) (Zdigits y) *)
apply (Zpower_lt_Zpower beta).
(* Goal: Z.lt (Z.pow (radix_val beta) (Z.sub d (Zpos xH))) (Z.pow (radix_val beta) (Zdigits n)) *)
now apply Zle_lt_trans with (Zabs n).
Qed.

Theorem Zdigits_abs :
  forall n, Zdigits (Zabs n) = Zdigits n.
Proof.
(* Goal: forall n : Z, @eq Z (Zdigits (Z.abs n)) (Zdigits n) *)
now intros [|n|n].
Qed.

Theorem Zdigits_gt_0 :
  forall n, n <> Z0 -> (0 < Zdigits n)%Z.
Proof.
(* Goal: forall (n : Z) (_ : not (@eq Z n Z0)), not (@eq Z (Zdigit n (Z.sub (Zdigits n) (Zpos xH))) Z0) *)
intros n Zn.
(* Goal: Z.lt Z0 (Zdigits n) *)
rewrite <- (Zdigits_abs n).
(* Goal: Z.lt Z0 (Zdigits (Z.abs n)) *)
assert (Hn: (0 < Zabs n)%Z).
(* Goal: Z.lt Z0 (Z.abs n) *)
(* Goal: Z.lt Z0 (Zdigits (Z.abs n)) *)
destruct n ; [|easy|easy].
(* Goal: Z.lt Z0 (Z.abs Z0) *)
(* Goal: Z.lt Z0 (Zdigits (Z.abs n)) *)
now elim Zn.
(* Goal: forall _ : and (Z.le (Z.pow (radix_val beta) (Z.sub (Zpos xH) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Zpos xH)))), and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Zpos xH) (Z.pow (radix_val beta) (Zpos xH)) u))) *)
destruct (Zabs n) as [|p|p] ; try easy ; clear.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
(* Goal: Z.lt Z0 (Zdigits_aux (Zpos p) (Zpos xH) (radix_val beta) (digits2_Pnat p)) *)
generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z).
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (digits2_Pnat p)) *)
induction (digits2_Pnat p).
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (if Z.ltb (Zpos p) z0 then z else Zdigits_aux (Zpos p) (Z.add z (Zpos xH)) (Z.mul (radix_val beta) z0) n) *)
intros.
(* Goal: Z.lt Z0 (if Z.ltb (Zpos p) z0 then z else Zdigits_aux (Zpos p) (Z.add z (Zpos xH)) (Z.mul (radix_val beta) z0) n) *)
case Zlt_bool.
(* Goal: Z.lt Z0 z *)
(* Goal: Z.lt Z0 (Zdigits_aux (Zpos p) (Z.add z (Zpos xH)) (Z.mul (radix_val beta) z0) n) *)
exact H.
(* Goal: Z.lt Z0 (Zdigits_aux (Zpos p) (Z.add z (Zpos xH)) (Z.mul (radix_val beta) z0) n) *)
apply IHn.
(* Goal: Z.lt Z0 (Z.add z (Zpos xH)) *)
now apply Zlt_lt_succ.
Qed.

Theorem Zdigits_ge_0 :
  forall n, (0 <= Zdigits n)%Z.
Proof.
(* Goal: forall n : Z, Z.le Z0 (Zdigits n) *)
intros n.
(* Goal: Z.le Z0 (Zdigits n) *)
destruct (Z_eq_dec n 0) as [H|H].
(* Goal: Z.le Z0 (Zdigits n) *)
(* Goal: Z.le Z0 (Zdigits n) *)
now rewrite H.
(* Goal: Z.le Z0 (Zdigits n) *)
apply Zlt_le_weak.
(* Goal: Z.lt Z0 (Zdigits n) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits n) (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits n) (Zpos xH)) (Zpos xH)))) *)
now apply Zdigits_gt_0.
Qed.

Theorem Zdigit_out :
  forall n k, (Zdigits n <= k)%Z ->
  Zdigit n k = Z0.
Proof.
(* Goal: forall (n k : Z) (_ : Z.le (Zdigits n) k), @eq Z (Zdigit n k) Z0 *)
intros n k Hk.
(* Goal: @eq Z (Zdigit n k) Z0 *)
apply Zdigit_ge_Zpower with (2 := Hk).
(* Goal: Z.lt (Z.abs y) (Z.pow (radix_val beta) (Zdigits y)) *)
(* Goal: Z.le Z0 (Z.add x (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add y (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zdigits_correct.
Qed.

Theorem Zdigit_digits :
  forall n, n <> Z0 ->
  Zdigit n (Zdigits n - 1) <> Z0.
Proof.
(* Goal: forall (n : Z) (_ : not (@eq Z n Z0)), not (@eq Z (Zdigit n (Z.sub (Zdigits n) (Zpos xH))) Z0) *)
intros n Zn.
(* Goal: not (@eq Z (Zdigit n (Z.sub (Zdigits n) (Zpos xH))) Z0) *)
apply Zdigit_not_0.
(* Goal: Z.le Z0 (Z.sub (Zdigits n) (Zpos xH)) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits n) (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits n) (Zpos xH)) (Zpos xH)))) *)
apply Zlt_0_le_0_pred.
(* Goal: Z.lt Z0 (Zdigits n) *)
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits n) (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits n) (Zpos xH)) (Zpos xH)))) *)
now apply Zdigits_gt_0.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits n) (Zpos xH))) (Z.abs n)) (Z.lt (Z.abs n) (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits n) (Zpos xH)) (Zpos xH)))) *)
ring_simplify (Zdigits n - 1 + 1)%Z.
(* Goal: Z.lt (Z.abs y) (Z.pow (radix_val beta) (Zdigits y)) *)
(* Goal: Z.le Z0 (Z.add x (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add y (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zdigits_correct.
Qed.

Theorem Zdigits_slice :
  forall n k l, (0 <= l)%Z ->
  (Zdigits (Zslice n k l) <= l)%Z.
Proof.
(* Goal: forall (n k l : Z) (_ : Z.le Z0 l), Z.le (Zdigits (Zslice n k l)) l *)
intros n k l Hl.
(* Goal: Z.le (Zdigits (Zslice n k l)) l *)
unfold Zslice.
(* Goal: Z.le (Zdigits (if Z.leb Z0 l then Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l) else Z0)) l *)
rewrite Zle_bool_true with (1 := Hl).
(* Goal: Z.le (Zdigits (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) l *)
destruct (Zdigits_correct (Z.rem (Zscale n (- k)) (Zpower beta l))) as (H1,H2).
(* Goal: Z.le (Zdigits (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) l *)
apply Zpower_lt_Zpower with beta.
(* Goal: Z.lt (Z.pow (radix_val beta) (Z.sub (Zdigits (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) (Zpos xH))) (Z.pow (radix_val beta) l) *)
apply Zle_lt_trans with (1 := H1).
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
rewrite <- (Zabs_eq (beta ^ l)) at 2 by apply Zpower_ge_0.
(* Goal: Z.lt (Z.abs (Z.rem (Zscale n (Z.opp k)) (Z.pow (radix_val beta) l))) (Z.abs (Z.pow (radix_val beta) l)) *)
apply Zrem_lt.
(* Goal: not (@eq Z (Z.pow (radix_val beta) l) Z0) *)
apply Zgt_not_eq.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
Qed.

Theorem Zdigits_mult_Zpower :
  forall m e,
  m <> Z0 -> (0 <= e)%Z ->
  Zdigits (m * Zpower beta e) = (Zdigits m + e)%Z.
Proof.
intros m e Hm He.
assert (H := Zdigits_correct m).
apply Zdigits_unique.
rewrite Z.abs_mul, Z.abs_pow, (Zabs_eq beta).
2: now apply Zlt_le_weak, radix_gt_0.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
split.
(* Goal: @eq Z (Z.add (Z.add k1 l1) (Z.sub k l1)) (Z.add k1 k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
replace (Zdigits m + e - 1)%Z with (Zdigits m - 1 + e)%Z by ring.
rewrite Zpower_plus with (2 := He).
apply Zmult_le_compat_r.
apply H.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
now apply Zlt_0_le_0_pred, Zdigits_gt_0.
rewrite Zpower_plus with (2 := He).
apply Zmult_lt_compat_r.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
now apply Zpower_gt_0.
apply H.
now apply Zlt_le_weak, Zdigits_gt_0.
Qed.

Theorem Zdigits_Zpower :
  forall e,
  (0 <= e)%Z ->
  Zdigits (Zpower beta e) = (e + 1)%Z.
Proof.
(* Goal: forall (e : Z) (_ : Z.le Z0 e), @eq Z (Zdigits (Z.pow (radix_val beta) e)) (Z.add e (Zpos xH)) *)
intros e He.
(* Goal: @eq Z (Zdigits (Z.pow (radix_val beta) e)) (Z.add e (Zpos xH)) *)
rewrite <- (Zmult_1_l (Zpower beta e)).
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
rewrite Zdigits_mult_Zpower ; try easy.
(* Goal: @eq Z (Z.add (Zdigits (Zpos xH)) e) (Z.add e (Zpos xH)) *)
apply Zplus_comm.
Qed.

Theorem Zdigits_le :
  forall x y,
  (0 <= x)%Z -> (x <= y)%Z ->
  (Zdigits x <= Zdigits y)%Z.
Proof.
(* Goal: forall (x y : Z) (_ : Z.le Z0 x) (_ : Z.le x y), Z.le (Zdigits x) (Zdigits y) *)
intros x y Zx Hxy.
(* Goal: Z.le (Zdigits x) (Zdigits y) *)
assert (Hx := Zdigits_correct x).
(* Goal: Z.le (Zdigits x) (Zdigits y) *)
assert (Hy := Zdigits_correct y).
(* Goal: Z.le (Zdigits x) (Zdigits y) *)
apply (Zpower_lt_Zpower beta).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
zify ; omega.
Qed.

Theorem lt_Zdigits :
  forall x y,
  (0 <= y)%Z ->
  (Zdigits x < Zdigits y)%Z ->
  (x < y)%Z.
Proof.
(* Goal: forall (x y : Z) (_ : Z.le Z0 y) (_ : Z.lt (Zdigits x) (Zdigits y)), Z.lt x y *)
intros x y Hy.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
cut (y <= x -> Zdigits y <= Zdigits x)%Z. omega.
(* Goal: forall _ : Z.le y x, Z.le (Zdigits y) (Zdigits x) *)
now apply Zdigits_le.
Qed.

Theorem Zpower_le_Zdigits :
  forall e x,
  (e < Zdigits x)%Z ->
  (Zpower beta e <= Zabs x)%Z.
Proof.
(* Goal: forall (e x : Z) (_ : Z.le (Z.pow (radix_val beta) e) (Z.abs x)), Z.lt e (Zdigits x) *)
intros e x Hex.
(* Goal: Z.lt (Z.abs x) (Z.pow (radix_val beta) e) *)
destruct (Zdigits_correct x) as [H1 H2].
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.abs x) *)
apply Zle_trans with (2 := H1).
(* Goal: Z.le (Z.pow (radix_val beta) e) (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
apply Zpower_le.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
clear -Hex ; omega.
Qed.

Theorem Zdigits_le_Zpower :
  forall e x,
  (Zabs x < Zpower beta e)%Z ->
  (Zdigits x <= e)%Z.
Proof.
(* Goal: forall (e x : Z) (_ : Z.lt (Z.abs x) (Z.pow (radix_val beta) e)), Z.le (Zdigits x) e *)
intros e x.
(* Goal: forall _ : Z.lt (Z.abs x) (Z.pow (radix_val beta) e), Z.le (Zdigits x) e *)
generalize (Zpower_le_Zdigits e x).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

Theorem Zpower_gt_Zdigits :
  forall e x,
  (Zdigits x <= e)%Z ->
  (Zabs x < Zpower beta e)%Z.
Proof.
(* Goal: forall (e x : Z) (_ : Z.le (Z.pow (radix_val beta) e) (Z.abs x)), Z.lt e (Zdigits x) *)
intros e x Hex.
(* Goal: Z.lt (Z.abs x) (Z.pow (radix_val beta) e) *)
destruct (Zdigits_correct x) as [H1 H2].
(* Goal: Z.lt (Z.abs x) (Z.pow (radix_val beta) e) *)
apply Zlt_le_trans with (1 := H2).
(* Goal: Z.le (Z.pow (radix_val beta) (Zdigits x)) (Z.pow (radix_val beta) e) *)
now apply Zpower_le.
Qed.

Theorem Zdigits_gt_Zpower :
  forall e x,
  (Zpower beta e <= Zabs x)%Z ->
  (e < Zdigits x)%Z.
Proof.
(* Goal: forall (e x : Z) (_ : Z.le (Z.pow (radix_val beta) e) (Z.abs x)), Z.lt e (Zdigits x) *)
intros e x Hex.
(* Goal: Z.lt e (Zdigits x) *)
generalize (Zpower_gt_Zdigits e x).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
Qed.

(** Number of digits of a product.

This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
*)

Theorem Zdigits_mult_strong :
  forall x y,
  (0 <= x)%Z -> (0 <= y)%Z ->
  (Zdigits (x + y + x * y) <= Zdigits x + Zdigits y)%Z.
Proof.
(* Goal: forall (x y : Z) (_ : Z.le Z0 x) (_ : Z.le Z0 y), Z.le (Zdigits (Z.add (Z.add x y) (Z.mul x y))) (Z.add (Zdigits x) (Zdigits y)) *)
intros x y Hx Hy.
(* Goal: Z.le (Zdigits (Z.add (Z.add x y) (Z.mul x y))) (Z.add (Zdigits x) (Zdigits y)) *)
apply Zdigits_le_Zpower.
(* Goal: Z.lt (Z.abs (Z.add (Z.add x y) (Z.mul x y))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
rewrite Zabs_eq.
(* Goal: Z.lt (Z.add (Z.add x y) (Z.mul x y)) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zlt_le_trans with ((x + 1) * (y + 1))%Z.
(* Goal: Z.lt (Z.add (Z.add x y) (Z.mul x y)) (Z.mul (Z.add x (Zpos xH)) (Z.add y (Zpos xH))) *)
(* Goal: Z.le (Z.mul (Z.add x (Zpos xH)) (Z.add y (Zpos xH))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
ring_simplify.
(* Goal: Z.lt (Z.add (Z.add (Z.mul x y) x) y) (Z.add (Z.add (Z.add (Z.mul x y) x) y) (Zpos xH)) *)
(* Goal: Z.le (Z.mul (Z.add x (Zpos xH)) (Z.add y (Zpos xH))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zle_lt_succ, Zle_refl.
(* Goal: Z.le (Z.mul (Z.add x (Zpos xH)) (Z.add y (Zpos xH))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
rewrite Zpower_plus by apply Zdigits_ge_0.
(* Goal: Z.le (Z.mul (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH)))) (Z.mul (Z.abs x) (Z.abs y)) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zmult_le_compat.
(* Goal: Z.le (Z.add y (Zpos xH)) (Z.pow (radix_val beta) (Zdigits y)) *)
(* Goal: Z.le Z0 (Z.add x (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add y (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zlt_le_succ.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
rewrite <- (Zabs_eq x) at 1 by easy.
(* Goal: Z.lt (Z.abs y) (Z.pow (radix_val beta) (Zdigits y)) *)
(* Goal: Z.le Z0 (Z.add x (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add y (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zdigits_correct.
(* Goal: Z.le (Z.add y (Zpos xH)) (Z.pow (radix_val beta) (Zdigits y)) *)
(* Goal: Z.le Z0 (Z.add x (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add y (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zlt_le_succ.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
rewrite <- (Zabs_eq y) at 1 by easy.
(* Goal: Z.lt (Z.abs y) (Z.pow (radix_val beta) (Zdigits y)) *)
(* Goal: Z.le Z0 (Z.add x (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add y (Zpos xH)) *)
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zdigits_correct.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
clear -Hx ; omega.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
clear -Hy ; omega.
(* Goal: Z.le Z0 (Z.add (Z.add x y) (Z.mul x y)) *)
change Z0 with (0 + 0 + 0)%Z.
(* Goal: Z.le (Z.add (Z.add Z0 Z0) Z0) (Z.add (Z.add x y) (Z.mul x y)) *)
apply Zplus_le_compat.
(* Goal: Z.le (Z.add (Z.add Z0 Z0) Z0) (Z.add (Z.add x y) (Z.mul x y)) *)
now apply Zplus_le_compat.
(* Goal: Z.le Z0 (Z.mul (Z.mul n n) (Z.pow (radix_val beta) k)) *)
(* Goal: Z.le Z0 (Z.mul n (Z.quot n (Z.pow (radix_val beta) (Z.opp k)))) *)
now apply Zmult_le_0_compat.
Qed.

Theorem Zdigits_mult :
  forall x y,
  (Zdigits (x * y) <= Zdigits x + Zdigits y)%Z.
Proof.
(* Goal: forall x y : Z, Z.le (Zdigits (Z.mul x y)) (Z.add (Zdigits x) (Zdigits y)) *)
intros x y.
(* Goal: Z.le (Zdigits (Z.mul x y)) (Z.add (Zdigits x) (Zdigits y)) *)
rewrite <- Zdigits_abs.
(* Goal: Z.le (Zdigits (Z.abs (Z.mul x y))) (Z.add (Zdigits x) (Zdigits y)) *)
rewrite <- (Zdigits_abs x).
(* Goal: Z.le (Zdigits (Z.abs (Z.mul x y))) (Z.add (Zdigits (Z.abs x)) (Zdigits y)) *)
rewrite <- (Zdigits_abs y).
(* Goal: Z.le (Zdigits (Z.abs (Z.mul x y))) (Z.add (Zdigits (Z.abs x)) (Zdigits (Z.abs y))) *)
apply Zle_trans with (Zdigits (Zabs x + Zabs y + Zabs x * Zabs y)).
(* Goal: Z.le (Zdigits (Z.abs (Z.mul x y))) (Zdigits (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y)))) *)
(* Goal: Z.le (Zdigits (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y)))) (Z.add (Zdigits (Z.abs x)) (Zdigits (Z.abs y))) *)
apply Zdigits_le.
(* Goal: Z.le Z0 (Z.abs (Z.mul x y)) *)
(* Goal: Z.le (Z.abs (Z.mul x y)) (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y))) *)
(* Goal: Z.le (Zdigits (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y)))) (Z.add (Zdigits (Z.abs x)) (Zdigits (Z.abs y))) *)
apply Zabs_pos.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits x) (Zpos xH)) (Z.sub (Zdigits y) (Zpos xH)))) (Z.abs (Z.mul x y)) *)
rewrite Zabs_Zmult.
(* Goal: Z.le (Z.mul (Z.abs x) (Z.abs y)) (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y))) *)
(* Goal: Z.le (Zdigits (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y)))) (Z.add (Zdigits (Z.abs x)) (Zdigits (Z.abs y))) *)
generalize (Zabs_pos x) (Zabs_pos y).
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
omega.
(* Goal: Z.le Z0 (Z.abs (Z.mul x y)) *)
(* Goal: Z.le (Z.abs (Z.mul x y)) (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y))) *)
(* Goal: Z.le (Zdigits (Z.add (Z.add (Z.abs x) (Z.abs y)) (Z.mul (Z.abs x) (Z.abs y)))) (Z.add (Zdigits (Z.abs x)) (Zdigits (Z.abs y))) *)
apply Zdigits_mult_strong ; apply Zabs_pos.
Qed.

Theorem Zdigits_mult_ge :
  forall x y,
  (x <> 0)%Z -> (y <> 0)%Z ->
  (Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z.
Proof.
(* Goal: forall (x y : Z) (_ : not (@eq Z x Z0)) (_ : not (@eq Z y Z0)), Z.le (Z.sub (Z.add (Zdigits x) (Zdigits y)) (Zpos xH)) (Zdigits (Z.mul x y)) *)
intros x y Zx Zy.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. omega.
(* Goal: Z.lt (Z.add (Z.sub (Zdigits x) (Zpos xH)) (Z.sub (Zdigits y) (Zpos xH))) (Zdigits (Z.mul x y)) *)
apply Zdigits_gt_Zpower.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits x) (Zpos xH)) (Z.sub (Zdigits y) (Zpos xH)))) (Z.abs (Z.mul x y)) *)
rewrite Zabs_Zmult.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.add (Z.sub (Zdigits x) (Zpos xH)) (Z.sub (Zdigits y) (Zpos xH)))) (Z.mul (Z.abs x) (Z.abs y)) *)
rewrite Zpower_exp.
(* Goal: Z.le (Z.mul (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH)))) (Z.mul (Z.abs x) (Z.abs y)) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zmult_le_compat.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) (Z.abs y) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_le_Zdigits.
(* Goal: Z.lt (Z.sub (Zdigits y) (Zpos xH)) (Zdigits y) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zlt_pred.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) (Z.abs y) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_le_Zdigits.
(* Goal: Z.lt (Z.sub (Zdigits y) (Zpos xH)) (Zdigits y) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits x) (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zlt_pred.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: Z.le Z0 (Z.pow (radix_val beta) (Z.sub (Zdigits y) (Zpos xH))) *)
(* Goal: Z.ge (Z.sub (Zdigits x) (Zpos xH)) Z0 *)
(* Goal: Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
apply Zpower_ge_0.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
generalize (Zdigits_gt_0 x). omega.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
generalize (Zdigits_gt_0 y). omega.
Qed.

Theorem Zdigits_div_Zpower :
  forall m e,
  (0 <= m)%Z ->
  (0 <= e <= Zdigits m)%Z ->
  Zdigits (m / Zpower beta e) = (Zdigits m - e)%Z.
Proof.
intros m e Hm He.
assert (H := Zdigits_correct m).
apply Zdigits_unique.
destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
  rewrite Zabs_eq in H by easy.
  destruct H as [H1 H2].
(* Goal: Z.lt (Z.abs (Z.add (Z.add x y) (Z.mul x y))) (Z.pow (radix_val beta) (Z.add (Zdigits x) (Zdigits y))) *)
  rewrite Zabs_eq.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
  split.
(* Goal: @eq Z (Z.add (Z.add k1 l1) (Z.sub k l1)) (Z.add k1 k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
  replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring.
  rewrite Z.pow_sub_r.
  2: apply Zgt_not_eq, radix_gt_0.
(* Goal: forall _ : forall _ : not (@eq Z y Z0), Z.lt Z0 (Zdigits y), Z.ge (Z.sub (Zdigits y) (Zpos xH)) Z0 *)
  2: clear -He He' ; omega.
  apply Z_div_le with (2 := H1).
  now apply Zlt_gt, Zpower_gt_0.
  apply Zmult_lt_reg_r with (Zpower beta e).
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Z.sub k e)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val beta) e) *)
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.sub k e) *)
  now apply Zpower_gt_0.
  apply Zle_lt_trans with m.
(* Goal: Z.le Z0 (Z.mul (Zscale (Zslice n (Z.add k1 l1) l2) l1) n) *)
(* Goal: Z.le Z0 (Z.mul n (Zslice n k1 l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
  rewrite Zmult_comm.
  apply Z_mult_div_ge.
  now apply Zlt_gt, Zpower_gt_0.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (Z.pow (radix_val beta) (Zpos xH)) (Z.pow (radix_val beta) v)) u) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Zdigits_aux (Zpos n) (Z.add v (Zpos xH)) (Z.mul (Z.pow (radix_val beta) (Zpos xH)) (Z.pow (radix_val beta) v)) u))) *)
  rewrite <- Zpower_plus.
(* Goal: @eq Z (Z.add (Z.add k1 l1) (Z.sub k l1)) (Z.add k1 k) *)
(* Goal: @eq Z (Z.add (Zdigit (Zslice n k1 l1) k) (Zdigit (Zslice n (Z.add k1 l1) l2) (Z.sub k l1))) (Zdigit n (Z.add k1 k)) *)
(* Goal: Z.le Z0 (Z.mul (Zslice n k1 l1) (Zscale (Zslice n (Z.add k1 l1) l2) l1)) *)
(* Goal: forall (k : Z) (_ : Z.le Z0 k), or (@eq Z (Zdigit (Zslice n k1 l1) k) Z0) (@eq Z (Zdigit (Zscale (Zslice n (Z.add k1 l1) l2) l1) k) Z0) *)
  now replace (Zdigits m - e + e)%Z with (Zdigits m) by ring.
(* Goal: Z.le Z0 (Z.sub k k') *)
(* Goal: @eq Z (Zdigit (Z.mul n (Z.pow (radix_val beta) k')) k) (Zdigit n (Z.sub k k')) *)
  now apply Zle_minus_le_0.
  apply He.
  apply Z_div_pos with (2 := Hm).
  now apply Zlt_gt, Zpower_gt_0.
rewrite He'.
rewrite (Zeq_minus _ (Zdigits m)) by reflexivity.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
simpl.
rewrite Zdiv_small.
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 O) *)
(* Goal: forall (z z0 : Z) (_ : Z.lt Z0 z), Z.lt Z0 (Zdigits_aux (Zpos p) z z0 (S n)) *)
easy.
(* Goal: and (Z.le (Z.pow (radix_val beta) (Z.sub (Z.add (Zpos xH) v) (Zpos xH))) (Zpos n)) (Z.lt (Zpos n) (Z.pow (radix_val beta) (Z.add (Z.of_nat u) (Z.add (Zpos xH) v)))) *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.le Z0 v *)
split.
exact Hm.
now rewrite <- (Zabs_eq m) at 1.
Qed.

End Fcore_digits.

(** Specialized version for computing the number of bits of an integer *)

Section Zdigits2.

Theorem Z_of_nat_S_digits2_Pnat :
  forall m : positive,
  Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
Proof.
(* Goal: forall m : positive, @eq Z (Zpos (digits2_pos m)) (Zdigits radix2 (Zpos m)) *)
intros m.
(* Goal: @eq Z (Z.of_nat (S (digits2_Pnat m))) (Zdigits radix2 (Zpos m)) *)
apply eq_sym, Zdigits_unique.
(* Goal: and (Z.le (Z.pow (radix_val radix2) (Z.of_nat (digits2_Pnat m))) (Z.abs (Zpos m))) (Z.lt (Z.abs (Zpos m)) (Zpower_nat (radix_val radix2) (S (digits2_Pnat m)))) *)
rewrite <- Zpower_nat_Z.
(* Goal: and (Z.le (Z.pow (radix_val radix2) (Z.sub (Z.of_nat (S (digits2_Pnat m))) (Zpos xH))) (Z.abs (Zpos m))) (Z.lt (Z.abs (Zpos m)) (Zpower_nat (radix_val radix2) (S (digits2_Pnat m)))) *)
rewrite Nat2Z.inj_succ.
(* Goal: and (Z.le (Z.pow (radix_val radix2) (Z.sub (Z.succ (Z.of_nat (digits2_Pnat m))) (Zpos xH))) (Z.abs (Zpos m))) (Z.lt (Z.abs (Zpos m)) (Zpower_nat (radix_val radix2) (S (digits2_Pnat m)))) *)
change (_ - 1)%Z with (Zpred (Zsucc (Z.of_nat (digits2_Pnat m)))).
(* Goal: and (Z.le (Z.pow (radix_val radix2) (Z.pred (Z.succ (Z.of_nat (digits2_Pnat m))))) (Z.abs (Zpos m))) (Z.lt (Z.abs (Zpos m)) (Zpower_nat (radix_val radix2) (S (digits2_Pnat m)))) *)
rewrite <- Zpred_succ.
(* Goal: and (Z.le (Z.pow (radix_val radix2) (Z.of_nat (digits2_Pnat m))) (Z.abs (Zpos m))) (Z.lt (Z.abs (Zpos m)) (Zpower_nat (radix_val radix2) (S (digits2_Pnat m)))) *)
rewrite <- Zpower_nat_Z.
(* Goal: and (Z.le (Zpower_nat (radix_val radix2) (digits2_Pnat m)) (Z.abs (Zpos m))) (Z.lt (Z.abs (Zpos m)) (Zpower_nat (radix_val radix2) (S (digits2_Pnat m)))) *)
apply digits2_Pnat_correct.
Qed.

Fixpoint digits2_pos (n : positive) : positive :=
  match n with
  | xH => xH
  | xO p => Psucc (digits2_pos p)
  | xI p => Psucc (digits2_pos p)
  end.

Theorem Zpos_digits2_pos :
  forall m : positive,
  Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).
Proof.
(* Goal: forall m : positive, @eq Z (Zpos (digits2_pos m)) (Zdigits radix2 (Zpos m)) *)
intros m.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Zdigits radix2 (Zpos m)) *)
rewrite <- Z_of_nat_S_digits2_Pnat.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Z.of_nat (S (digits2_Pnat m))) *)
unfold Z.of_nat.
(* Goal: @eq Z (Zpos (digits2_pos m)) (Zpos (Pos.of_succ_nat (digits2_Pnat m))) *)
apply f_equal.
induction m ; simpl ; try easy ;
  apply f_equal, IHm.
Qed.

Definition Zdigits2 n :=
  match n with
  | Z0 => n
  | Zpos p => Zpos (digits2_pos p)
  | Zneg p => Zpos (digits2_pos p)
  end.

Lemma Zdigits2_Zdigits :
  forall n, Zdigits2 n = Zdigits radix2 n.
Proof.
intros [|p|p] ; try easy ;
  apply Zpos_digits2_pos.
Qed.

End Zdigits2.
