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

Section Zmissing.

(** About Z *)
Theorem Zopp_le_cancel :
  forall x y : Z,
  (-y <= -x)%Z -> Zle x y.
Proof.
(* Goal: forall (x y : Z) (_ : Z.le y x), @eq bool (Z.ltb x y) false *)
intros x y Hxy.
(* Goal: Z.le x y *)
apply Zplus_le_reg_r with (-x - y)%Z.
(* Goal: Z.le (Z.add x (Z.sub (Z.opp x) y)) (Z.add y (Z.sub (Z.opp x) y)) *)
now ring_simplify.
Qed.

Theorem Zgt_not_eq :
  forall x y : Z,
  (y < x)%Z -> (x <> y)%Z.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), not (@eq Z x y) *)
intros x y H Hn.
(* Goal: False *)
apply Zlt_irrefl with x.
(* Goal: Z.lt x x *)
now rewrite Hn at 1.
Qed.

End Zmissing.

Section Proof_Irrelevance.

Scheme eq_dep_elim := Induction for eq Sort Type.

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

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

End Proof_Irrelevance.

Section Even_Odd.

(** Zeven, used for rounding to nearest, ties to even *)
Definition Zeven (n : Z) :=
  match n with
  | Zpos (xO _) => true
  | Zneg (xO _) => true
  | Z0 => true
  | _ => false
  end.

Theorem Zeven_mult :
  forall x y, Zeven (x * y) = orb (Zeven x) (Zeven y).
Proof.
(* Goal: forall x y : Z, @eq bool (Zeven (Z.mul x y)) (orb (Zeven x) (Zeven y)) *)
now intros [|[xp|xp|]|[xp|xp|]] [|[yp|yp|]|[yp|yp|]].
Qed.

Theorem Zeven_opp :
  forall x, Zeven (- x) = Zeven x.
Proof.
(* Goal: forall x : Z, @eq bool (Zeven (Z.opp x)) (Zeven x) *)
now intros [|[n|n|]|[n|n|]].
Qed.

Theorem Zeven_ex :
  forall x, exists p, x = (2 * p + if Zeven x then 0 else 1)%Z.
Proof.
(* Goal: forall x : Z, @ex Z (fun p : Z => @eq Z x (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven x then Z0 else Zpos xH))) *)
intros [|[n|n|]|[n|n|]].
(* Goal: @ex Z (fun p : Z => @eq Z (Zpos xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zpos xH) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xI n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xI n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
now exists Z0.
(* Goal: @ex Z (fun p : Z => @eq Z (Zpos (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zpos (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zpos xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zpos xH) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xI n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xI n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
now exists (Zpos n).
(* Goal: @ex Z (fun p : Z => @eq Z (Zpos (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zpos (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zpos xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zpos xH) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xI n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xI n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
now exists (Zpos n).
(* Goal: @ex Z (fun p : Z => @eq Z (Zpos xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zpos xH) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xI n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xI n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
now exists Z0.
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xI n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xI n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
exists (Zneg n - 1)%Z.
(* Goal: @eq Z (Zneg (xI n)) (Z.add (Z.mul (Zpos (xO xH)) (Z.sub (Zneg n) (Zpos xH))) (if Zeven (Zneg (xI n)) then Z0 else Zpos xH)) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
change (2 * Zneg n - 1 = 2 * (Zneg n - 1) + 1)%Z.
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
ring.
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg (xO n)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg (xO n)) then Z0 else Zpos xH))) *)
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
now exists (Zneg n).
(* Goal: @ex Z (fun p : Z => @eq Z (Zneg xH) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Zneg xH) then Z0 else Zpos xH))) *)
now exists (-1)%Z.
Qed.

Theorem Zeven_2xp1 :
  forall n, Zeven (2 * n + 1) = false.
Proof.
(* Goal: forall n : Z, @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) n) (Zpos xH))) false *)
intros n.
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) n) (Zpos xH))) false *)
destruct (Zeven_ex (2 * n + 1)) as (p, Hp).
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) n) (Zpos xH))) false *)
revert Hp.
(* Goal: forall _ : @eq Z (Z.add (Z.mul (Zpos (xO xH)) n) (Zpos xH)) (Z.add (Z.mul (Zpos (xO xH)) p) (if Zeven (Z.add (Z.mul (Zpos (xO xH)) n) (Zpos xH)) then Z0 else Zpos xH)), @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) n) (Zpos xH))) false *)
case (Zeven (2 * n + 1)) ; try easy.
(* Goal: not (@eq Z x y) *)
intros H.
(* Goal: @eq bool true false *)
apply False_ind.
(* Goal: forall _ : forall _ : Z.le a Z0, @eq Z (Z.abs a) (Z.opp a), and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
omega.
Qed.

Theorem Zeven_plus :
  forall x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: @eq bool (Zeven (Z.add x y)) (Bool.eqb (Zeven x) (Zeven y)) *)
destruct (Zeven_ex x) as (px, Hx).
(* Goal: @eq bool (Zeven (Z.add x y)) (Bool.eqb (Zeven x) (Zeven y)) *)
rewrite Hx at 1.
(* Goal: @eq bool (Zeven (Z.add (Z.add (Z.mul (Zpos (xO xH)) px) (if Zeven x then Z0 else Zpos xH)) y)) (Bool.eqb (Zeven x) (Zeven y)) *)
destruct (Zeven_ex y) as (py, Hy).
(* Goal: @eq bool (Zeven (Z.add (Z.add (Z.mul (Zpos (xO xH)) px) (if Zeven x then Z0 else Zpos xH)) y)) (Bool.eqb (Zeven x) (Zeven y)) *)
rewrite Hy at 1.
replace (2 * px + (if Zeven x then 0 else 1) + (2 * py + (if Zeven y then 0 else 1)))%Z
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
  with (2 * (px + py) + ((if Zeven x then 0 else 1) + (if Zeven y then 0 else 1)))%Z by ring.
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (if Zeven x then Z0 else Zpos xH) (if Zeven y then Z0 else Zpos xH)))) (Bool.eqb (Zeven x) (Zeven y)) *)
case (Zeven x) ; case (Zeven y).
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add Z0 Z0))) (Bool.eqb true true) *)
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add Z0 (Zpos xH)))) (Bool.eqb true false) *)
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (Zpos xH) Z0))) (Bool.eqb false true) *)
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (Zpos xH) (Zpos xH)))) (Bool.eqb false false) *)
rewrite Zplus_0_r.
(* Goal: @eq bool (Zeven (Z.mul (Zpos (xO xH)) (Z.add (Z.add px py) (Zpos xH)))) (Bool.eqb false false) *)
now rewrite Zeven_mult.
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (Zpos xH) Z0))) (Bool.eqb false true) *)
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (Zpos xH) (Zpos xH)))) (Bool.eqb false false) *)
apply Zeven_2xp1.
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (Zpos xH) Z0))) (Bool.eqb false true) *)
(* Goal: @eq bool (Zeven (Z.add (Z.mul (Zpos (xO xH)) (Z.add px py)) (Z.add (Zpos xH) (Zpos xH)))) (Bool.eqb false false) *)
apply Zeven_2xp1.
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
replace (2 * (px + py) + (1 + 1))%Z with (2 * (px + py + 1))%Z by ring.
(* Goal: @eq bool (Zeven (Z.mul (Zpos (xO xH)) (Z.add (Z.add px py) (Zpos xH)))) (Bool.eqb false false) *)
now rewrite Zeven_mult.
Qed.

End Even_Odd.

Section Zpower.

Theorem Zpower_plus :
  forall n k1 k2, (0 <= k1)%Z -> (0 <= k2)%Z ->
  Zpower n (k1 + k2) = (Zpower n k1 * Zpower n k2)%Z.
Proof.
(* Goal: forall (n k1 k2 : Z) (_ : Z.le Z0 k1) (_ : Z.le Z0 k2), @eq Z (Z.pow n (Z.add k1 k2)) (Z.mul (Z.pow n k1) (Z.pow n k2)) *)
intros n k1 k2 H1 H2.
(* Goal: @eq Z (Z.pow n (Z.add k1 k2)) (Z.mul (Z.pow n k1) (Z.pow n k2)) *)
now apply Zpower_exp ; apply Zle_ge.
Qed.

Theorem Zpower_Zpower_nat :
  forall b e, (0 <= e)%Z ->
  Zpower b e = Zpower_nat b (Zabs_nat e).
Proof.
(* Goal: forall (b e : Z) (_ : Z.le Z0 e), @eq Z (Z.pow b e) (Zpower_nat b (Z.abs_nat e)) *)
intros b [|e|e] He.
(* Goal: @eq Z (Z.abs (cond_Zopp false m)) (Z.abs m) *)
apply refl_equal.
(* Goal: @eq Z (Z.pow b (Zpos e)) (Zpower_nat b (Z.abs_nat (Zpos e))) *)
(* Goal: @eq Z (Z.pow b (Zneg e)) (Zpower_nat b (Z.abs_nat (Zneg e))) *)
apply Zpower_pos_nat.
(* Goal: @eq Z (Z.pow b (Zneg e)) (Zpower_nat b (Z.abs_nat (Zneg e))) *)
elim He.
(* Goal: @eq Z (Z.abs (cond_Zopp false m)) (Z.abs m) *)
apply refl_equal.
Qed.

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

Theorem Zpower_pos_gt_0 :
  forall b p, (0 < b)%Z ->
  (0 < Zpower_pos b p)%Z.
Proof.
(* Goal: forall (b : Z) (p : positive) (_ : Z.lt Z0 b), Z.lt Z0 (Z.pow_pos b p) *)
intros b p Hb.
(* Goal: Z.lt (Zpos xH) (Z.pow_pos (radix_val r) p) *)
rewrite Zpower_pos_nat.
(* Goal: forall _ : lt O (Pos.to_nat p), Z.lt (Zpos xH) (Zpower_nat (radix_val r) (Pos.to_nat p)) *)
induction (nat_of_P p).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) (S n)) *)
rewrite Zpower_nat_S.
(* Goal: Z.lt Z0 (Z.mul b (Zpower_nat b n)) *)
now apply Zmult_lt_0_compat.
Qed.

Theorem Zeven_Zpower :
  forall b e, (0 < e)%Z ->
  Zeven (Zpower b e) = Zeven b.
Proof.
(* Goal: forall (b e : Z) (_ : Z.lt Z0 e), @eq bool (Zeven (Z.pow b e)) (Zeven b) *)
intros b e He.
(* Goal: @eq bool (Zeven (Z.pow b e)) (Zeven b) *)
case_eq (Zeven b) ; intros Hb.
(* b even *)
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
replace e with (e - 1 + 1)%Z by ring.
(* Goal: @eq bool (Zeven (Z.pow b (Z.add (Z.sub e (Zpos xH)) (Zpos xH)))) true *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
rewrite Zpower_exp.
(* Goal: @eq bool (Zeven (Z.mul b (nat_rect (fun _ : nat => Z) (Zpos xH) (fun _ : nat => Z.mul b) n))) false *)
(* Goal: Z.le Z0 e *)
rewrite Zeven_mult.
(* Goal: @eq bool (orb (Zeven (Z.pow b (Z.sub e (Zpos xH)))) (Zeven (Z.pow b (Zpos xH)))) true *)
(* Goal: Z.ge (Z.sub e (Zpos xH)) Z0 *)
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
replace (Zeven (b ^ 1)) with true.
(* Goal: @eq bool (orb (Zeven (Z.pow b (Z.sub e (Zpos xH)))) true) true *)
(* Goal: @eq bool true (Zeven (Z.pow b (Zpos xH))) *)
(* Goal: Z.ge (Z.sub e (Zpos xH)) Z0 *)
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
apply Bool.orb_true_r.
(* Goal: @eq bool true (Zeven (Z.pow b (Zpos xH))) *)
(* Goal: Z.ge (Z.sub e (Zpos xH)) Z0 *)
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
unfold Zpower, Zpower_pos. simpl.
(* Goal: @eq bool true (Zeven (Z.mul b (Zpos xH))) *)
(* Goal: Z.ge (Z.sub e (Zpos xH)) Z0 *)
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
now rewrite Zmult_1_r.
(* Goal: forall _ : forall _ : Z.le a Z0, @eq Z (Z.abs a) (Z.opp a), and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
omega.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
discriminate.
(* b odd *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
rewrite Zpower_Zpower_nat.
(* Goal: @eq bool (Zeven (Zpower_nat b (Z.abs_nat e))) false *)
(* Goal: Z.le Z0 e *)
induction (Zabs_nat e).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
unfold Zpower_nat. simpl.
(* Goal: @eq bool (Zeven (Z.mul b (nat_rect (fun _ : nat => Z) (Zpos xH) (fun _ : nat => Z.mul b) n))) false *)
(* Goal: Z.le Z0 e *)
rewrite Zeven_mult.
(* Goal: @eq bool (orb (Zeven b) (Zeven (nat_rect (fun _ : nat => Z) (Zpos xH) (fun _ : nat => Z.mul b) n))) false *)
(* Goal: Z.le Z0 e *)
now rewrite Hb.
(* Goal: Z.le m Z0 *)
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
now apply Zlt_le_weak.
Qed.

Theorem Zeven_Zpower_odd :
  forall b e, (0 <= e)%Z -> Zeven b = false ->
  Zeven (Zpower b e) = false.
Proof.
(* Goal: forall (b e : Z) (_ : Z.le Z0 e) (_ : @eq bool (Zeven b) false), @eq bool (Zeven (Z.pow b e)) false *)
intros b e He Hb.
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
destruct (Z_le_lt_eq_dec _ _ He) as [He'|He'].
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
rewrite <- Hb.
(* Goal: @eq bool (Zeven (Z.pow b e)) (Zeven b) *)
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
now apply Zeven_Zpower.
(* Goal: @eq bool (Zeven (Z.pow b e)) false *)
now rewrite <- He'.
Qed.

(** The radix must be greater than 1 *)
Record radix := { radix_val :> Z ; radix_prop : Zle_bool 2 radix_val = true }.

Theorem radix_val_inj :
  forall r1 r2, radix_val r1 = radix_val r2 -> r1 = r2.
Proof.
(* Goal: forall (r1 r2 : radix) (_ : @eq Z (radix_val r1) (radix_val r2)), @eq radix r1 r2 *)
intros (r1, H1) (r2, H2) H.
(* Goal: @eq radix (Build_radix r1 H1) (Build_radix r2 H2) *)
simpl in H.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
revert H1.
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
rewrite H.
(* Goal: forall H1 : @eq bool (Z.leb (Zpos (xO xH)) r2) true, @eq radix (Build_radix r2 H1) (Build_radix r2 H2) *)
intros H1.
(* Goal: @eq (prod Z Z) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.add (Z.modulo (Z.mul (Zpos a) (Zpos (xO xH))) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b))))) *)
apply f_equal.
(* Goal: @eq (@eq bool (Z.leb (Zpos (xO xH)) r2) true) H1 H2 *)
apply eqbool_irrelevance.
Qed.

Definition radix2 := Build_radix 2 (refl_equal _).

Variable r : radix.

Theorem radix_gt_0 : (0 < r)%Z.
Proof.
(* Goal: Z.lt (Zpos xH) v *)
apply Zlt_le_trans with 2%Z.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.le (Zpos (xO xH)) (radix_val r) *)
apply Zle_bool_imp_le.
(* Goal: @eq bool (Z.leb (Zpos (xO xH)) (radix_val r)) true *)
apply r.
Qed.

Theorem radix_gt_1 : (1 < r)%Z.
Proof.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
destruct r as (v, Hr). simpl.
(* Goal: Z.lt (Zpos xH) v *)
apply Zlt_le_trans with 2%Z.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.le (Zpos (xO xH)) (radix_val r) *)
now apply Zle_bool_imp_le.
Qed.

Theorem Zpower_gt_1 :
  forall p,
  (0 < p)%Z ->
  (1 < Zpower r p)%Z.
Proof.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
intros [|p|p] Hp ; try easy.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
simpl.
(* Goal: Z.lt (Zpos xH) (Z.pow_pos (radix_val r) p) *)
rewrite Zpower_pos_nat.
(* Goal: Z.lt (Zpos xH) (Zpower_nat (radix_val r) (Pos.to_nat p)) *)
generalize (lt_O_nat_of_P p).
(* Goal: forall _ : lt O (Pos.to_nat p), Z.lt (Zpos xH) (Zpower_nat (radix_val r) (Pos.to_nat p)) *)
induction (nat_of_P p).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: forall _ : Z.lt (Zneg p) Z0, Z.lt (Z.pow (radix_val r) (Zneg p)) (Z.pow (radix_val r) e2) *)
intros _.
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) (S n)) *)
rewrite Zpower_nat_S.
(* Goal: Z.lt (Zpos xH) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
assert (0 < Zpower_nat r n)%Z.
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) n) *)
(* Goal: Z.lt (Zpos xH) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
clear.
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) n) *)
(* Goal: Z.lt (Zpos xH) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
induction n.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) (S n)) *)
rewrite Zpower_nat_S.
(* Goal: Z.lt Z0 (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
apply Zmult_lt_0_compat with (2 := IHn).
(* Goal: Z.lt Z0 (radix_val r) *)
apply radix_gt_0.
(* Goal: Z.lt (Zpos xH) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
apply Zle_lt_trans with (1 * Zpower_nat r n)%Z.
(* Goal: Z.le (Zpos xH) (Z.mul (Zpos xH) (Zpower_nat (radix_val r) n)) *)
(* Goal: Z.lt (Z.mul (Zpos xH) (Zpower_nat (radix_val r) n)) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
rewrite Zmult_1_l.
(* Goal: Z.le (Zpos xH) (Zpower_nat (radix_val r) n) *)
(* Goal: Z.lt (Z.mul (Zpos xH) (Zpower_nat (radix_val r) n)) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
now apply (Zlt_le_succ 0).
(* Goal: Z.lt (Z.mul (Zpos xH) (Zpower_nat (radix_val r) n)) (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
apply Zmult_lt_compat_r with (1 := H).
(* Goal: Z.lt (Zpos xH) (radix_val r) *)
apply radix_gt_1.
Qed.

Theorem Zpower_gt_0 :
  forall p,
  (0 <= p)%Z ->
  (0 < Zpower r p)%Z.
Proof.
(* Goal: forall (p : Z) (_ : Z.le Z0 p), Z.lt Z0 (Z.pow (radix_val r) p) *)
intros p Hp.
(* Goal: Z.lt Z0 (Z.pow (radix_val r) p) *)
rewrite Zpower_Zpower_nat with (1 := Hp).
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) (Z.abs_nat p)) *)
induction (Zabs_nat p).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.lt Z0 (Zpower_nat (radix_val r) (S n)) *)
rewrite Zpower_nat_S.
(* Goal: Z.lt Z0 (Z.mul (radix_val r) (Zpower_nat (radix_val r) n)) *)
apply Zmult_lt_0_compat with (2 := IHn).
(* Goal: Z.lt Z0 (radix_val r) *)
apply radix_gt_0.
Qed.

Theorem Zpower_ge_0 :
  forall e,
  (0 <= Zpower r e)%Z.
Proof.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
intros [|e|e] ; try easy.
(* Goal: Z.le Z0 (Z.pow (radix_val r) (Zpos e)) *)
apply Zlt_le_weak.
(* Goal: Z.lt (Z.pow (radix_val r) (Zneg p)) (Z.pow (radix_val r) e2) *)
now apply Zpower_gt_0.
Qed.

Theorem Zpower_le :
  forall e1 e2, (e1 <= e2)%Z ->
  (Zpower r e1 <= Zpower r e2)%Z.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Z.lt (Z.pow (radix_val r) (Z.sub e1 (Zpos xH))) (Z.pow (radix_val r) e2)), Z.le e1 e2 *)
intros e1 e2 He.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
replace e2 with (e2 - e1 + e1)%Z by ring.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) (Z.add (Z.sub e2 e1) e1)) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
rewrite Zpower_plus with (2 := H1).
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.mul (Z.pow (radix_val r) (Z.sub e2 e1)) (Z.pow (radix_val r) e1)) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
rewrite <- (Zmult_1_l (r ^ e1)) at 1.
(* Goal: Z.le (Z.mul (Zpos xH) (Z.pow (radix_val r) e1)) (Z.mul (Z.pow (radix_val r) (Z.sub e2 e1)) (Z.pow (radix_val r) e1)) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply Zmult_le_compat_r.
(* Goal: Z.le (Zpos xH) (Z.pow (radix_val r) (Z.sub e2 e1)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val r) e1) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply (Zlt_le_succ 0).
(* Goal: Z.lt Z0 (Z.pow (radix_val r) (Z.sub e2 e1)) *)
(* Goal: Z.le Z0 (Z.pow (radix_val r) e1) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply Zpower_gt_0.
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
now apply Zle_minus_le_0.
(* Goal: Z.le (Z.pow (radix_val r) (Zneg e1)) (Z.pow (radix_val r) e2) *)
apply Zpower_ge_0.
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
now apply Zle_minus_le_0.
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
clear He.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
destruct e1 as [|e1|e1] ; try easy.
(* Goal: Z.le (Z.pow (radix_val r) (Zneg e1)) (Z.pow (radix_val r) e2) *)
apply Zpower_ge_0.
Qed.

Theorem Zpower_lt :
  forall e1 e2, (0 <= e2)%Z -> (e1 < e2)%Z ->
  (Zpower r e1 < Zpower r e2)%Z.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Z.le Z0 e2) (_ : Z.lt e1 e2), Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
intros e1 e2 He2 He.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
replace e2 with (e2 - e1 + e1)%Z by ring.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) (Z.add (Z.sub e2 e1) e1)) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
rewrite Zpower_plus with (2 := H1).
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.mul (Z.pow (radix_val r) (Z.sub e2 e1)) (Z.pow (radix_val r) e1)) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
rewrite Zmult_comm.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.mul (Z.pow (radix_val r) e1) (Z.pow (radix_val r) (Z.sub e2 e1))) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
rewrite <- (Zmult_1_r (r ^ e1)) at 1.
(* Goal: Z.lt (Z.mul (Z.pow (radix_val r) e1) (Zpos xH)) (Z.mul (Z.pow (radix_val r) e1) (Z.pow (radix_val r) (Z.sub e2 e1))) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply Zmult_lt_compat2.
(* Goal: and (Z.le Z0 a) (Z.lt a b) *)
(* Goal: @eq Z (Z.rem a b) a *)
split.
(* Goal: Z.lt (Z.pow (radix_val r) (Zneg p)) (Z.pow (radix_val r) e2) *)
now apply Zpower_gt_0.
(* Goal: Z.le (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e1) *)
(* Goal: and (Z.lt Z0 (Zpos xH)) (Z.lt (Zpos xH) (Z.pow (radix_val r) (Z.sub e2 e1))) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply Zle_refl.
(* Goal: and (Z.le Z0 a) (Z.lt a b) *)
(* Goal: @eq Z (Z.rem a b) a *)
split.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.lt (Zpos xH) (Z.pow (radix_val r) (Z.sub e2 e1)) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply Zpower_gt_1.
(* Goal: forall _ : forall _ : Z.le a Z0, @eq Z (Z.abs a) (Z.opp a), and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
clear -He ; omega.
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
apply Zle_minus_le_0.
(* Goal: Z.le m Z0 *)
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
now apply Zlt_le_weak.
(* Goal: Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
revert H1.
(* Goal: forall _ : Z.lt e1 Z0, Z.lt (Z.pow (radix_val r) e1) (Z.pow (radix_val r) e2) *)
clear -He2.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
destruct e1 ; try easy.
(* Goal: forall _ : Z.lt (Zneg p) Z0, Z.lt (Z.pow (radix_val r) (Zneg p)) (Z.pow (radix_val r) e2) *)
intros _.
(* Goal: Z.lt (Z.pow (radix_val r) (Zneg p)) (Z.pow (radix_val r) e2) *)
now apply Zpower_gt_0.
Qed.

Theorem Zpower_lt_Zpower :
  forall e1 e2,
  (Zpower r (e1 - 1) < Zpower r e2)%Z ->
  (e1 <= e2)%Z.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Z.lt (Z.pow (radix_val r) (Z.sub e1 (Zpos xH))) (Z.pow (radix_val r) e2)), Z.le e1 e2 *)
intros e1 e2 He.
(* Goal: Z.le e1 e2 *)
apply Znot_gt_le.
(* Goal: not (@eq Z x y) *)
intros H.
(* Goal: False *)
apply Zlt_not_le with (1 := He).
(* Goal: Z.le (Z.pow (radix_val r) e2) (Z.pow (radix_val r) (Z.sub e1 (Zpos xH))) *)
apply Zpower_le.
(* Goal: forall _ : forall _ : Z.le a Z0, @eq Z (Z.abs a) (Z.opp a), and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
clear -H ; omega.
Qed.

End Zpower.

Section Div_Mod.

Theorem Zmod_mod_mult :
  forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
  Zmod (Zmod n (a * b)) b = Zmod n b.
Proof.
(* Goal: forall (n a b : Z) (_ : Z.lt Z0 a) (_ : Z.le Z0 b), @eq Z (Z.modulo (Z.modulo n (Z.mul a b)) b) (Z.modulo n b) *)
intros n a [|b|b] Ha Hb.
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a Z0)) Z0) (Z.modulo n Z0) *)
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zpos b))) (Zpos b)) (Z.modulo n (Zpos b)) *)
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zneg b))) (Zneg b)) (Z.modulo n (Zneg b)) *)
now rewrite 2!Zmod_0_r.
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zpos b))) (Zpos b)) (Z.modulo n (Zpos b)) *)
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zneg b))) (Zneg b)) (Z.modulo n (Zneg b)) *)
rewrite (Zmod_eq n (a * Zpos b)).
(* Goal: @eq Z (Z.div (Z.sub n (Z.mul (Z.div n (Z.mul a b)) (Z.mul b a))) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite Zmult_assoc.
(* Goal: @eq Z (Z.div (Z.sub n (Z.mul (Z.mul (Z.div n (Z.mul a b)) b) a)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
unfold Zminus.
(* Goal: @eq Z (Z.div (Z.add n (Z.opp (Z.mul (Z.mul (Z.div n (Z.mul a b)) b) a))) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite Zopp_mult_distr_l.
(* Goal: @eq Z (Z.modulo (Z.add n (Z.mul (Z.opp (Z.mul (Z.div n (Z.mul a (Zpos b))) a)) (Zpos b))) (Zpos b)) (Z.modulo n (Zpos b)) *)
(* Goal: Z.gt (Z.mul a (Zpos b)) Z0 *)
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zneg b))) (Zneg b)) (Z.modulo n (Zneg b)) *)
apply Z_mod_plus.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.gt (Z.mul a (Zpos b)) Z0 *)
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zneg b))) (Zneg b)) (Z.modulo n (Zneg b)) *)
apply Zmult_gt_0_compat.
(* Goal: Z.gt b Z0 *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
now apply Zlt_gt.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: @eq Z (Z.modulo (Z.modulo n (Z.mul a (Zneg b))) (Zneg b)) (Z.modulo n (Zneg b)) *)
now elim Hb.
Qed.

Theorem ZOmod_eq :
  forall a b,
  Z.rem a b = (a - Z.quot a b * b)%Z.
Proof.
(* Goal: forall a b : positive, @eq (prod Z Z) (Zpos_div_eucl_aux a b) (Z.pos_div_eucl a (Zpos b)) *)
intros a b.
(* Goal: @eq Z (Z.rem a b) (Z.sub a (Z.mul (Z.quot a b) b)) *)
rewrite (Z.quot_rem' a b) at 2.
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
ring.
Qed.

Theorem ZOmod_mod_mult :
  forall n a b,
  Z.rem (Z.rem n (a * b)) b = Z.rem n b.
Proof.
(* Goal: forall n a b : Z, @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
intros n a b.
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul a b)) b) (Z.rem n b) *)
assert (Z.rem n (a * b) = n + - (Z.quot n (a * b) * a) * b)%Z.
(* Goal: @eq Z (Z.rem n (Z.mul a b)) (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot n (Z.mul a b)) a)) b)) *)
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul a b)) b) (Z.rem n b) *)
rewrite <- Zopp_mult_distr_l.
(* Goal: @eq Z (Z.rem n (Z.mul a b)) (Z.add n (Z.opp (Z.mul (Z.mul (Z.quot n (Z.mul a b)) a) b))) *)
(* Goal: @eq Z (Z.rem (Z.rem n (Z.mul a b)) b) (Z.rem n b) *)
rewrite <- Zmult_assoc.
(* Goal: @eq Z (Z.rem (Z.quot n a) b) (Z.add (Z.quot n a) (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b))) *)
(* Goal: Z.le Z0 (Z.mul (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) n) *)
apply ZOmod_eq.
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
rewrite H.
(* Goal: @eq Z (Z.rem (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot n (Z.mul a b)) a)) b)) b) (Z.rem n b) *)
apply Z_rem_plus.
(* Goal: Z.le Z0 (Z.mul (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) n) *)
rewrite <- H.
(* Goal: Z.le Z0 (Z.mul (Z.rem n (Z.mul a b)) n) *)
apply Zrem_sgn2.
Qed.

Theorem Zdiv_mod_mult :
  forall n a b, (0 <= a)%Z -> (0 <= b)%Z ->
  (Zdiv (Zmod n (a * b)) a) = Zmod (Zdiv n a) b.
Proof.
(* Goal: forall (n a b : Z) (_ : Z.le Z0 a) (_ : Z.le Z0 b), @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
intros n a b Ha Hb.
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|Hb'].
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite (Zmod_eq n (a * b)).
(* Goal: @eq Z (Z.div (Z.sub n (Z.mul (Z.div n (Z.mul a b)) (Z.mul a b))) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite (Zmult_comm a b) at 2.
(* Goal: @eq Z (Z.div (Z.sub n (Z.mul (Z.div n (Z.mul a b)) (Z.mul b a))) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite Zmult_assoc.
(* Goal: @eq Z (Z.div (Z.sub n (Z.mul (Z.mul (Z.div n (Z.mul a b)) b) a)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
unfold Zminus.
(* Goal: @eq Z (Z.div (Z.add n (Z.opp (Z.mul (Z.mul (Z.div n (Z.mul a b)) b) a))) a) (Z.modulo (Z.div n a) b) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite Zopp_mult_distr_l.
(* Goal: Z.gt b Z0 *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite Z_div_plus by now apply Zlt_gt.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite <- Zdiv_Zdiv by easy.
(* Goal: @eq Z (cond_Zopp (Z.ltb m Z0) m) (Z.abs m) *)
apply sym_eq.
(* Goal: @eq Z (Z.modulo (Z.div n a) b) (Z.add (Z.div n a) (Z.opp (Z.mul (Z.div (Z.div n a) b) b))) *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
apply Zmod_eq.
(* Goal: Z.gt b Z0 *)
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
now apply Zlt_gt.
(* Goal: Z.gt (Z.mul a b) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
now apply Zmult_gt_0_compat ; apply Zlt_gt.
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite <- Hb'.
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a Z0)) a) (Z.modulo (Z.div n a) Z0) *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite Zmult_0_r, 2!Zmod_0_r.
(* Goal: @eq Z (Z.div Z0 a) Z0 *)
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
apply Zdiv_0_l.
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul a b)) a) (Z.modulo (Z.div n a) b) *)
rewrite <- Ha'.
(* Goal: @eq Z (Z.div (Z.modulo n (Z.mul Z0 b)) Z0) (Z.modulo (Z.div n Z0) b) *)
now rewrite 2!Zdiv_0_r, Zmod_0_l.
Qed.

Theorem ZOdiv_mod_mult :
  forall n a b,
  (Z.quot (Z.rem n (a * b)) a) = Z.rem (Z.quot n a) b.
Proof.
(* Goal: forall n a b : Z, @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
intros n a b.
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
destruct (Z_eq_dec a 0) as [Za|Za].
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
rewrite Za.
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul Z0 b)) Z0) (Z.rem (Z.quot n Z0) b) *)
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
now rewrite 2!Zquot_0_r, Zrem_0_l.
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
assert (Z.rem n (a * b) = n + - (Z.quot (Z.quot n a) b * b) * a)%Z.
(* Goal: @eq Z (Z.rem n (Z.mul a b)) (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) *)
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
rewrite (ZOmod_eq n (a * b)) at 1.
(* Goal: @eq Z (Z.sub n (Z.mul (Z.quot n (Z.mul a b)) (Z.mul a b))) (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) *)
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
rewrite Zquot_Zquot.
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
ring.
(* Goal: @eq Z (Z.quot (Z.rem n (Z.mul a b)) a) (Z.rem (Z.quot n a) b) *)
rewrite H.
(* Goal: @eq Z (Z.quot (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) a) (Z.rem (Z.quot n a) b) *)
rewrite Z_quot_plus with (2 := Za).
(* Goal: @eq Z (cond_Zopp (Z.ltb m Z0) m) (Z.abs m) *)
apply sym_eq.
(* Goal: @eq Z (Z.rem (Z.quot n a) b) (Z.add (Z.quot n a) (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b))) *)
(* Goal: Z.le Z0 (Z.mul (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) n) *)
apply ZOmod_eq.
(* Goal: Z.le Z0 (Z.mul (Z.add n (Z.mul (Z.opp (Z.mul (Z.quot (Z.quot n a) b) b)) a)) n) *)
rewrite <- H.
(* Goal: Z.le Z0 (Z.mul (Z.rem n (Z.mul a b)) n) *)
apply Zrem_sgn2.
Qed.

Theorem ZOdiv_small_abs :
  forall a b,
  (Zabs a < b)%Z -> Z.quot a b = Z0.
Proof.
(* Goal: forall (a b : Z) (_ : Z.lt (Z.abs a) b), @eq Z (Z.rem a b) a *)
intros a b Ha.
(* Goal: @eq Z (Z.rem a b) a *)
destruct (Zle_or_lt 0 a) as [H|H].
(* Goal: @eq Z (Z.quot (Z.opp a) b) Z0 *)
apply Zquot_small.
(* Goal: and (Z.le Z0 a) (Z.lt a b) *)
(* Goal: @eq Z (Z.rem a b) a *)
split.
(* Goal: Z.le y x *)
(* Goal: Z.le y x *)
exact H.
(* Goal: Z.lt a b *)
(* Goal: @eq Z (Z.rem a b) a *)
now rewrite Zabs_eq in Ha.
(* Goal: @eq Z (Z.rem a b) a *)
apply Zopp_inj.
(* Goal: @eq Z (Z.opp (Z.quot a b)) (Z.opp Z0) *)
rewrite <- Zquot_opp_l, Zopp_0.
(* Goal: @eq Z (Z.quot (Z.opp a) b) Z0 *)
apply Zquot_small.
(* Goal: and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
generalize (Zabs_non_eq a).
(* Goal: forall _ : forall _ : Z.le a Z0, @eq Z (Z.abs a) (Z.opp a), and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
omega.
Qed.

Theorem ZOmod_small_abs :
  forall a b,
  (Zabs a < b)%Z -> Z.rem a b = a.
Proof.
(* Goal: forall (a b : Z) (_ : Z.lt (Z.abs a) b), @eq Z (Z.rem a b) a *)
intros a b Ha.
(* Goal: @eq Z (Z.rem a b) a *)
destruct (Zle_or_lt 0 a) as [H|H].
(* Goal: @eq Z (Z.rem (Z.opp a) b) (Z.opp a) *)
apply Zrem_small.
(* Goal: and (Z.le Z0 a) (Z.lt a b) *)
(* Goal: @eq Z (Z.rem a b) a *)
split.
(* Goal: Z.le y x *)
(* Goal: Z.le y x *)
exact H.
(* Goal: Z.lt a b *)
(* Goal: @eq Z (Z.rem a b) a *)
now rewrite Zabs_eq in Ha.
(* Goal: @eq Z (Z.rem a b) a *)
apply Zopp_inj.
(* Goal: @eq Z (Z.opp (Z.rem a b)) (Z.opp a) *)
rewrite <- Zrem_opp_l.
(* Goal: @eq Z (Z.rem (Z.opp a) b) (Z.opp a) *)
apply Zrem_small.
(* Goal: and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
generalize (Zabs_non_eq a).
(* Goal: forall _ : forall _ : Z.le a Z0, @eq Z (Z.abs a) (Z.opp a), and (Z.le Z0 (Z.opp a)) (Z.lt (Z.opp a) b) *)
omega.
Qed.

Theorem ZOdiv_plus :
  forall a b c, (0 <= a * b)%Z ->
  (Z.quot (a + b) c = Z.quot a c + Z.quot b c + Z.quot (Z.rem a c + Z.rem b c) c)%Z.
Proof.
(* Goal: forall (a b c : Z) (_ : Z.le Z0 (Z.mul a b)), @eq Z (Z.quot (Z.add a b) c) (Z.add (Z.add (Z.quot a c) (Z.quot b c)) (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c)) *)
intros a b c Hab.
(* Goal: @eq Z (Z.quot (Z.add a b) c) (Z.add (Z.add (Z.quot a c) (Z.quot b c)) (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c)) *)
destruct (Z_eq_dec c 0) as [Zc|Zc].
(* Goal: @eq Z (Z.quot (Z.add a b) c) (Z.add (Z.add (Z.quot a c) (Z.quot b c)) (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c)) *)
(* Goal: @eq Z (Z.quot (Z.add a b) c) (Z.add (Z.add (Z.quot a c) (Z.quot b c)) (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c)) *)
now rewrite Zc, 4!Zquot_0_r.
(* Goal: @eq Z (Z.quot (Z.add a b) c) (Z.add (Z.add (Z.quot a c) (Z.quot b c)) (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c)) *)
apply Zmult_reg_r with (1 := Zc).
(* Goal: @eq Z (Z.mul (Z.quot (Z.add a b) c) c) (Z.mul (Z.add (Z.add (Z.quot a c) (Z.quot b c)) (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c)) c) *)
rewrite 2!Zmult_plus_distr_l.
(* Goal: @eq Z (Z.mul (Z.quot (Z.add a b) c) c) (Z.add (Z.add (Z.mul (Z.quot a c) c) (Z.mul (Z.quot b c) c)) (Z.mul (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c) c)) *)
assert (forall d, Z.quot d c * c = d - Z.rem d c)%Z.
(* Goal: forall d : Z, @eq Z (Z.mul (Z.quot d c) c) (Z.sub d (Z.rem d c)) *)
(* Goal: @eq Z (Z.mul (Z.quot (Z.add a b) c) c) (Z.add (Z.add (Z.mul (Z.quot a c) c) (Z.mul (Z.quot b c) c)) (Z.mul (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c) c)) *)
intros d.
(* Goal: @eq Z (Z.mul (Z.quot d c) c) (Z.sub d (Z.rem d c)) *)
(* Goal: @eq Z (Z.mul (Z.quot (Z.add a b) c) c) (Z.add (Z.add (Z.mul (Z.quot a c) c) (Z.mul (Z.quot b c) c)) (Z.mul (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c) c)) *)
rewrite ZOmod_eq.
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
ring.
(* Goal: @eq Z (Z.mul (Z.quot (Z.add a b) c) c) (Z.add (Z.add (Z.mul (Z.quot a c) c) (Z.mul (Z.quot b c) c)) (Z.mul (Z.quot (Z.add (Z.rem a c) (Z.rem b c)) c) c)) *)
rewrite 4!H.
(* Goal: @eq Z (Z.sub (Z.add a b) (Z.rem (Z.add a b) c)) (Z.add (Z.add (Z.sub a (Z.rem a c)) (Z.sub b (Z.rem b c))) (Z.sub (Z.add (Z.rem a c) (Z.rem b c)) (Z.rem (Z.add (Z.rem a c) (Z.rem b c)) c))) *)
rewrite <- Zplus_rem with (1 := Hab).
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
ring.
Qed.

End Div_Mod.

Section Same_sign.

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

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

Theorem Zsame_sign_imp :
  forall u v,
  (0 < u -> 0 <= v)%Z ->
  (0 < -u -> 0 <= -v)%Z ->
  (0 <= u * v)%Z.
Proof.
(* Goal: forall (u v : Z) (_ : forall _ : Z.lt Z0 u, Z.le Z0 v) (_ : forall _ : Z.lt Z0 (Z.opp u), Z.le Z0 (Z.opp v)), Z.le Z0 (Z.mul u v) *)
intros [|u|u] v Hp Hn.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.le Z0 (Z.mul (Zpos u) (Z.opp v)) *)
(* Goal: @eq Z (Z.mul (Zpos u) (Z.opp v)) (Z.mul (Zneg u) v) *)
apply Zmult_le_0_compat.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.le Z0 v *)
(* Goal: Z.le Z0 (Z.mul (Zneg u) v) *)
now apply Hp.
(* Goal: Z.le Z0 (Z.mul (Zneg u) v) *)
replace (Zneg u * v)%Z with (Zpos u * (-v))%Z.
(* Goal: Z.le Z0 (Z.mul (Zpos u) (Z.opp v)) *)
(* Goal: @eq Z (Z.mul (Zpos u) (Z.opp v)) (Z.mul (Zneg u) v) *)
apply Zmult_le_0_compat.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: Z.le Z0 (Z.opp v) *)
(* Goal: @eq Z (Z.mul (Zpos u) (Z.opp v)) (Z.mul (Zneg u) v) *)
now apply Hn.
(* Goal: @eq Z (Z.mul (Zpos u) (Z.opp v)) (Z.mul (Zneg u) v) *)
rewrite <- Zopp_mult_distr_r.
(* Goal: @eq Z (Z.opp (Z.mul (Zpos u) v)) (Z.mul (Zneg u) v) *)
apply Zopp_mult_distr_l.
Qed.

Theorem Zsame_sign_odiv :
  forall u v, (0 <= v)%Z ->
  (0 <= u * Z.quot u v)%Z.
Proof.
(* Goal: forall (u v : Z) (_ : Z.le Z0 v), Z.le Z0 (Z.mul u (Z.quot u v)) *)
intros u v Hv.
(* Goal: Z.le Z0 (Z.mul u (Z.quot u v)) *)
apply Zsame_sign_imp ; intros Hu.
(* Goal: Z.le Z0 (Z.quot (Z.opp u) v) *)
apply Z_quot_pos with (2 := Hv).
(* Goal: Z.le m Z0 *)
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
now apply Zlt_le_weak.
(* Goal: Z.le Z0 (Z.opp (Z.quot u v)) *)
rewrite <- Zquot_opp_l.
(* Goal: Z.le Z0 (Z.quot (Z.opp u) v) *)
apply Z_quot_pos with (2 := Hv).
(* Goal: Z.le m Z0 *)
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
now apply Zlt_le_weak.
Qed.

End Same_sign.

(** Boolean comparisons *)

Section Zeq_bool.

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

Theorem Zeq_bool_spec :
  forall x y, Zeq_bool_prop x y (Zeq_bool x y).
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: Zeq_bool_prop x y (Zeq_bool x y) *)
generalize (Zeq_is_eq_bool x y).
(* Goal: forall _ : iff (@eq Z x y) (@eq bool (Zeq_bool x y) true), Zeq_bool_prop x y (Zeq_bool x y) *)
case (Zeq_bool x y) ; intros (H1, H2) ; constructor.
(* Goal: Z.lt x y *)
(* Goal: Z.le y x *)
now apply H2.
(* Goal: not (@eq Z x y) *)
intros H.
(* Goal: False *)
specialize (H1 H).
(* Goal: False *)
discriminate H1.
Qed.

Theorem Zeq_bool_true :
  forall x y, x = y -> Zeq_bool x y = true.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: forall _ : @eq Z x y, @eq bool (Zeq_bool x y) true *)
apply -> Zeq_is_eq_bool.
Qed.

Theorem Zeq_bool_false :
  forall x y, x <> y -> Zeq_bool x y = false.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: forall _ : not (@eq Z x y), @eq bool (Zeq_bool x y) false *)
generalize (proj2 (Zeq_is_eq_bool x y)).
(* Goal: forall (_ : forall _ : @eq bool (Zeq_bool x y) true, @eq Z x y) (_ : not (@eq Z x y)), @eq bool (Zeq_bool x y) false *)
case Zeq_bool.
(* Goal: forall (_ : forall _ : @eq bool true true, @eq Z x y) (_ : not (@eq Z x y)), @eq bool true false *)
(* Goal: forall (_ : forall _ : @eq bool false true, @eq Z x y) (_ : not (@eq Z x y)), @eq bool false false *)
intros He Hn.
(* Goal: @eq bool true false *)
(* Goal: forall (_ : forall _ : @eq bool false true, @eq Z x y) (_ : not (@eq Z x y)), @eq bool false false *)
elim Hn.
(* Goal: @eq Z x y *)
(* Goal: forall (_ : forall _ : @eq bool false true, @eq Z x y) (_ : not (@eq Z x y)), @eq bool false false *)
now apply He.
(* Goal: forall (_ : forall _ : @eq bool false true, @eq Z x y) (_ : not (@eq Z x y)), @eq bool false false *)
now intros _ _.
Qed.

End Zeq_bool.

Section Zle_bool.

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

Theorem Zle_bool_spec :
  forall x y, Zle_bool_prop x y (Zle_bool x y).
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: Zle_bool_prop x y (Z.leb x y) *)
generalize (Zle_is_le_bool x y).
(* Goal: forall _ : iff (Z.le x y) (@eq bool (Z.leb x y) true), Zle_bool_prop x y (Z.leb x y) *)
case Zle_bool ; intros (H1, H2) ; constructor.
(* Goal: Z.lt x y *)
(* Goal: Z.le y x *)
now apply H2.
(* Goal: Z.lt y x *)
destruct (Zle_or_lt x y) as [H|H].
(* Goal: False *)
now specialize (H1 H).
(* Goal: Z.le y x *)
(* Goal: Z.le y x *)
exact H.
Qed.

Theorem Zle_bool_true :
  forall x y : Z,
  (x <= y)%Z -> Zle_bool x y = true.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: forall _ : Z.le x y, @eq bool (Z.leb x y) true *)
apply (proj1 (Zle_is_le_bool x y)).
Qed.

Theorem Zle_bool_false :
  forall x y : Z,
  (y < x)%Z -> Zle_bool x y = false.
Proof.
(* Goal: forall (x y : Z) (_ : Z.le y x), @eq bool (Z.ltb x y) false *)
intros x y Hxy.
(* Goal: @eq bool (Z.leb x y) false *)
generalize (Zle_cases x y).
(* Goal: not (@eq Z x y) *)
case Zle_bool ; intros H.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
elim (Zlt_irrefl x).
(* Goal: Z.lt x x *)
(* Goal: @eq bool false false *)
now apply Zle_lt_trans with y.
(* Goal: @eq Z (Z.abs (cond_Zopp false m)) (Z.abs m) *)
apply refl_equal.
Qed.

End Zle_bool.

Section Zlt_bool.

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

Theorem Zlt_bool_spec :
  forall x y, Zlt_bool_prop x y (Zlt_bool x y).
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: Zlt_bool_prop x y (Z.ltb x y) *)
generalize (Zlt_is_lt_bool x y).
(* Goal: forall _ : iff (Z.lt x y) (@eq bool (Z.ltb x y) true), Zlt_bool_prop x y (Z.ltb x y) *)
case Zlt_bool ; intros (H1, H2) ; constructor.
(* Goal: Z.lt x y *)
(* Goal: Z.le y x *)
now apply H2.
(* Goal: Z.le y x *)
destruct (Zle_or_lt y x) as [H|H].
(* Goal: Z.le y x *)
(* Goal: Z.le y x *)
exact H.
(* Goal: False *)
now specialize (H1 H).
Qed.

Theorem Zlt_bool_true :
  forall x y : Z,
  (x < y)%Z -> Zlt_bool x y = true.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: forall _ : Z.lt x y, @eq bool (Z.ltb x y) true *)
apply (proj1 (Zlt_is_lt_bool x y)).
Qed.

Theorem Zlt_bool_false :
  forall x y : Z,
  (y <= x)%Z -> Zlt_bool x y = false.
Proof.
(* Goal: forall (x y : Z) (_ : Z.le y x), @eq bool (Z.ltb x y) false *)
intros x y Hxy.
(* Goal: @eq bool (Z.ltb x y) false *)
generalize (Zlt_cases x y).
(* Goal: not (@eq Z x y) *)
case Zlt_bool ; intros H.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
elim (Zlt_irrefl x).
(* Goal: Z.lt x x *)
(* Goal: @eq bool false false *)
now apply Zlt_le_trans with y.
(* Goal: @eq Z (Z.abs (cond_Zopp false m)) (Z.abs m) *)
apply refl_equal.
Qed.

Theorem negb_Zle_bool :
  forall x y : Z,
  negb (Zle_bool x y) = Zlt_bool y x.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: not (@eq Z x y) *)
case Zle_bool_spec ; intros H.
(* Goal: @eq bool (negb true) (Z.ltb y x) *)
(* Goal: @eq bool (negb false) (Z.ltb y x) *)
now rewrite Zlt_bool_false.
(* Goal: @eq bool (negb false) (Z.ltb y x) *)
now rewrite Zlt_bool_true.
Qed.

Theorem negb_Zlt_bool :
  forall x y : Z,
  negb (Zlt_bool x y) = Zle_bool y x.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: not (@eq Z x y) *)
case Zlt_bool_spec ; intros H.
(* Goal: @eq bool (negb true) (Z.leb y x) *)
(* Goal: @eq bool (negb false) (Z.leb y x) *)
now rewrite Zle_bool_false.
(* Goal: @eq bool (negb false) (Z.leb y x) *)
now rewrite Zle_bool_true.
Qed.

End Zlt_bool.

Section Zcompare.

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

Theorem Zcompare_spec :
  forall x y, Zcompare_prop x y (Zcompare x y).
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: Zcompare_prop x y (Z.compare x y) *)
destruct (Z_dec x y) as [[H|H]|H].
(* Goal: Zcompare_prop x y (Z.compare x y) *)
(* Goal: Zcompare_prop x y (Z.compare x y) *)
(* Goal: Zcompare_prop x y (Z.compare x y) *)
generalize (Zlt_compare _ _ H).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
case (Zcompare x y) ; try easy.
(* Goal: forall _ : @eq comparison Eq Eq, Zcompare_prop x y Eq *)
now constructor.
(* Goal: Zcompare_prop x y (Z.compare x y) *)
(* Goal: Zcompare_prop x y (Z.compare x y) *)
generalize (Zgt_compare _ _ H).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
case (Zcompare x y) ; try easy.
(* Goal: forall _ : True, Zcompare_prop x y Gt *)
(* Goal: Zcompare_prop x y (Z.compare x y) *)
constructor.
(* Goal: Z.lt y x *)
(* Goal: Zcompare_prop x y (Z.compare x y) *)
now apply Zgt_lt.
(* Goal: Zcompare_prop x y (Z.compare x y) *)
generalize (proj2 (Zcompare_Eq_iff_eq _ _) H).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
case (Zcompare x y) ; try easy.
(* Goal: forall _ : @eq comparison Eq Eq, Zcompare_prop x y Eq *)
now constructor.
Qed.

Theorem Zcompare_Lt :
  forall x y,
  (x < y)%Z -> Zcompare x y = Lt.
Proof.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
Qed.

Theorem Zcompare_Eq :
  forall x y,
  (x = y)%Z -> Zcompare x y = Eq.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: forall _ : @eq Z x y, @eq comparison (Z.compare x y) Eq *)
apply <- Zcompare_Eq_iff_eq.
Qed.

Theorem Zcompare_Gt :
  forall x y,
  (y < x)%Z -> Zcompare x y = Gt.
Proof.
(* Goal: forall (x y : Z) (_ : Z.lt y x), @eq comparison (Z.compare x y) Gt *)
intros x y.
(* Goal: forall _ : Z.lt y x, @eq comparison (Z.compare x y) Gt *)
apply Zlt_gt.
Qed.

End Zcompare.

Section cond_Zopp.

Definition cond_Zopp (b : bool) m := if b then Zopp m else m.

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

Theorem cond_Zopp_Zlt_bool :
  forall m,
  cond_Zopp (Zlt_bool m 0) m = Zabs m.
Proof.
(* Goal: forall m : Z, @eq Z (cond_Zopp (Z.ltb m Z0) m) (Z.abs m) *)
intros m.
(* Goal: @eq Z (cond_Zopp (Z.ltb m Z0) m) (Z.abs m) *)
apply sym_eq.
(* Goal: @eq Z (Z.abs m) (cond_Zopp (Z.ltb m Z0) m) *)
case Zlt_bool_spec ; intros Hm.
(* Goal: @eq Z (Z.abs m) (cond_Zopp true m) *)
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
apply Zabs_non_eq.
(* Goal: Z.le m Z0 *)
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
now apply Zlt_le_weak.
(* Goal: @eq Z (Z.abs m) (cond_Zopp false m) *)
now apply Zabs_eq.
Qed.

End cond_Zopp.

Section fast_pow_pos.

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

Theorem Zfast_pow_pos_correct :
  forall v e, Zfast_pow_pos v e = Zpower_pos v e.
Proof.
(* Goal: forall (v : Z) (e : positive), @eq Z (Zfast_pow_pos v e) (Z.pow_pos v e) *)
intros v e.
(* Goal: @eq Z (Zfast_pow_pos v e) (Z.pow_pos v e) *)
rewrite <- (Zmult_1_r (Zfast_pow_pos v e)).
(* Goal: @eq Z (Z.mul (Zfast_pow_pos v e) (Zpos xH)) (Z.pow_pos v e) *)
unfold Z.pow_pos.
(* Goal: @eq Z (Z.mul (Zfast_pow_pos v e) (Zpos xH)) (Pos.iter Z (Z.mul v) (Zpos xH) e) *)
generalize 1%Z.
(* Goal: forall z : Z, @eq Z (Z.mul (Zfast_pow_pos v e) z) (Pos.iter Z (Z.mul v) z e) *)
revert v.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
induction e ; intros v f ; simpl.
- rewrite <- 2!IHe.
(* Goal: @eq Z (Z.mul (Z.square (Zfast_pow_pos v e)) f) (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f)) *)
  rewrite Z.square_spec.
(* Goal: @eq Z (Z.mul (Z.mul v (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e))) f) (Z.mul v (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f))) *)
  ring.
- rewrite <- 2!IHe.
(* Goal: @eq Z (Z.mul (Z.square (Zfast_pow_pos v e)) f) (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f)) *)
  rewrite Z.square_spec.
(* Goal: @eq Z (Z.mul (Z.mul (Zfast_pow_pos v e) (Zfast_pow_pos v e)) f) (Z.mul (Zfast_pow_pos v e) (Z.mul (Zfast_pow_pos v e) f)) *)
  apply eq_sym, Zmult_assoc.
- apply eq_refl.
Qed.

End fast_pow_pos.

Section faster_div.

Lemma Zdiv_eucl_unique :
  forall a b,
  Zdiv_eucl a b = (Zdiv a b, Zmod a b).
Proof.
(* Goal: forall a b : positive, @eq (prod Z Z) (Zpos_div_eucl_aux a b) (Z.pos_div_eucl a (Zpos b)) *)
intros a b.
(* Goal: @eq (prod Z Z) (Z.div_eucl a b) (@pair Z Z (Z.div a b) (Z.modulo a b)) *)
unfold Zdiv, Zmod.
(* Goal: @eq (prod Z Z) (Z.div_eucl a b) (@pair Z Z (let (q, _) := Z.div_eucl a b in q) (let (_, r) := Z.div_eucl a b in r)) *)
now case Zdiv_eucl.
Qed.

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

Lemma Zpos_div_eucl_aux1_correct :
  forall a b,
  Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Zpos b).
Proof.
(* Goal: forall a b : positive, @eq (prod Z Z) (Zpos_div_eucl_aux a b) (Z.pos_div_eucl a (Zpos b)) *)
intros a b.
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a b) (Z.pos_div_eucl a (Zpos b)) *)
revert a.
(* Goal: forall a : positive, @eq (prod Z Z) (Zpos_div_eucl_aux1 a b) (Z.pos_div_eucl a (Zpos b)) *)
induction b ; intros a.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
- easy.
- change (Z.pos_div_eucl a (Zpos b~0)) with (Zdiv_eucl (Zpos a) (Zpos b~0)).
(* Goal: @eq (prod Z Z) match Pos.compare a b with | Eq => @pair Z Z (Zpos xH) Z0 | Lt => @pair Z Z Z0 (Zpos a) | Gt => Zpos_div_eucl_aux1 a b end (Z.div_eucl (Zpos a) (Zpos b)) *)
  rewrite Zdiv_eucl_unique.
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a (xO b)) (@pair Z Z (Z.div (Zpos a) (Zpos (xO b))) (Z.modulo (Zpos a) (Zpos (xO b)))) *)
  change (Zpos b~0) with (2 * Zpos b)%Z.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
  rewrite Z.rem_mul_r by easy.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
  rewrite <- Zdiv_Zdiv by easy.
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a (xO b)) (@pair Z Z (Z.div (Z.div (Zpos a) (Zpos (xO xH))) (Zpos b)) (Z.add (Z.modulo (Zpos a) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.div (Zpos a) (Zpos (xO xH))) (Zpos b))))) *)
  destruct a as [a|a|].
  + change (Zpos_div_eucl_aux1 a~1 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r + 1)%Z).
(* Goal: @eq (prod Z Z) (let (q, r) := Zpos_div_eucl_aux1 a b in @pair Z Z q (Z.mul (Zpos (xO xH)) r)) (@pair Z Z (Z.div (Z.div (Zpos (xO a)) (Zpos (xO xH))) (Zpos b)) (Z.add (Z.modulo (Zpos (xO a)) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.div (Zpos (xO a)) (Zpos (xO xH))) (Zpos b))))) *)
    rewrite IHb. clear IHb.
(* Goal: @eq (prod Z Z) (Z.pos_div_eucl a (Zpos b)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
    change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
(* Goal: @eq (prod Z Z) match Pos.compare a b with | Eq => @pair Z Z (Zpos xH) Z0 | Lt => @pair Z Z Z0 (Zpos a) | Gt => Zpos_div_eucl_aux1 a b end (Z.div_eucl (Zpos a) (Zpos b)) *)
    rewrite Zdiv_eucl_unique.
    change (Zpos a~1) with (1 + 2 * Zpos a)%Z.
(* Goal: @eq (prod Z Z) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) (@pair Z Z (Z.div (Z.div (Z.mul (Zpos (xO xH)) (Zpos a)) (Zpos (xO xH))) (Zpos b)) (Z.add (Z.modulo (Z.mul (Zpos (xO xH)) (Zpos a)) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.div (Z.mul (Zpos (xO xH)) (Zpos a)) (Zpos (xO xH))) (Zpos b))))) *)
    rewrite (Zmult_comm 2 (Zpos a)).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
    rewrite Z_div_plus_full by easy.
(* Goal: @eq (prod Z Z) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.add (Z.modulo (Z.mul (Zpos a) (Zpos (xO xH))) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b))))) *)
    apply f_equal.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b))) (Zpos xH)) (Z.add (Z.modulo (Z.add (Zpos xH) (Z.mul (Zpos a) (Zpos (xO xH)))) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.add (Z.div (Zpos xH) (Zpos (xO xH))) (Zpos a)) (Zpos b)))) *)
    rewrite Z_mod_plus_full.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b))) (Zpos xH)) (Z.add (Z.modulo (Zpos xH) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.add (Z.div (Zpos xH) (Zpos (xO xH))) (Zpos a)) (Zpos b)))) *)
    apply Zplus_comm.
  + change (Zpos_div_eucl_aux1 a~0 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r)%Z).
(* Goal: @eq (prod Z Z) (let (q, r) := Zpos_div_eucl_aux1 a b in @pair Z Z q (Z.mul (Zpos (xO xH)) r)) (@pair Z Z (Z.div (Z.div (Zpos (xO a)) (Zpos (xO xH))) (Zpos b)) (Z.add (Z.modulo (Zpos (xO a)) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.div (Zpos (xO a)) (Zpos (xO xH))) (Zpos b))))) *)
    rewrite IHb. clear IHb.
(* Goal: @eq (prod Z Z) (Z.pos_div_eucl a (Zpos b)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
    change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
(* Goal: @eq (prod Z Z) match Pos.compare a b with | Eq => @pair Z Z (Zpos xH) Z0 | Lt => @pair Z Z Z0 (Zpos a) | Gt => Zpos_div_eucl_aux1 a b end (Z.div_eucl (Zpos a) (Zpos b)) *)
    rewrite Zdiv_eucl_unique.
(* Goal: @eq (prod Z Z) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) (@pair Z Z (Z.div (Z.div (Zpos (xO a)) (Zpos (xO xH))) (Zpos b)) (Z.add (Z.modulo (Zpos (xO a)) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.div (Zpos (xO a)) (Zpos (xO xH))) (Zpos b))))) *)
    change (Zpos a~0) with (2 * Zpos a)%Z.
(* Goal: @eq (prod Z Z) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) (@pair Z Z (Z.div (Z.div (Z.mul (Zpos (xO xH)) (Zpos a)) (Zpos (xO xH))) (Zpos b)) (Z.add (Z.modulo (Z.mul (Zpos (xO xH)) (Zpos a)) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Z.div (Z.mul (Zpos (xO xH)) (Zpos a)) (Zpos (xO xH))) (Zpos b))))) *)
    rewrite (Zmult_comm 2 (Zpos a)).
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
    rewrite Z_div_mult_full by easy.
(* Goal: @eq (prod Z Z) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.add (Z.modulo (Z.mul (Zpos a) (Zpos (xO xH))) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b))))) *)
    apply f_equal.
(* Goal: @eq Z (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b))) (Z.add (Z.modulo (Z.mul (Zpos a) (Zpos (xO xH))) (Zpos (xO xH))) (Z.mul (Zpos (xO xH)) (Z.modulo (Zpos a) (Zpos b)))) *)
    now rewrite Z_mod_mult.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
  + easy.
- change (Z.pos_div_eucl a 1) with (Zdiv_eucl (Zpos a) 1).
(* Goal: @eq (prod Z Z) match Pos.compare a b with | Eq => @pair Z Z (Zpos xH) Z0 | Lt => @pair Z Z Z0 (Zpos a) | Gt => Zpos_div_eucl_aux1 a b end (Z.div_eucl (Zpos a) (Zpos b)) *)
  rewrite Zdiv_eucl_unique.
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a xH) (@pair Z Z (Z.div (Zpos a) (Zpos xH)) (Z.modulo (Zpos a) (Zpos xH))) *)
  now rewrite Zdiv_1_r, Zmod_1_r.
Qed.

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

Lemma Zpos_div_eucl_aux_correct :
  forall a b,
  Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Zpos b).
Proof.
(* Goal: forall a b : positive, @eq (prod Z Z) (Zpos_div_eucl_aux a b) (Z.pos_div_eucl a (Zpos b)) *)
intros a b.
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux a b) (Z.pos_div_eucl a (Zpos b)) *)
unfold Zpos_div_eucl_aux.
(* Goal: @eq (prod Z Z) (Z.pos_div_eucl a (Zpos b)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
(* Goal: @eq (prod Z Z) match Pos.compare a b with | Eq => @pair Z Z (Zpos xH) Z0 | Lt => @pair Z Z Z0 (Zpos a) | Gt => Zpos_div_eucl_aux1 a b end (Z.div_eucl (Zpos a) (Zpos b)) *)
rewrite Zdiv_eucl_unique.
(* Goal: not (@eq Z x y) *)
case Pos.compare_spec ; intros H.
(* Goal: @eq (prod Z Z) (@pair Z Z (Zpos xH) Z0) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
(* Goal: @eq (prod Z Z) (@pair Z Z Z0 (Zpos a)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a b) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
now rewrite H, Z_div_same, Z_mod_same.
(* Goal: @eq (prod Z Z) (@pair Z Z Z0 (Zpos a)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a b) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
now rewrite Zdiv_small, Zmod_small by (split ; easy).
(* Goal: @eq (prod Z Z) (Zpos_div_eucl_aux1 a b) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
rewrite Zpos_div_eucl_aux1_correct.
(* Goal: @eq (prod Z Z) (Z.pos_div_eucl a (Zpos b)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
(* Goal: @eq (prod Z Z) (Z.div_eucl (Zpos a) (Zpos b)) (@pair Z Z (Z.div (Zpos a) (Zpos b)) (Z.modulo (Zpos a) (Zpos b))) *)
apply Zdiv_eucl_unique.
Qed.

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

Theorem Zfast_div_eucl_correct :
  forall a b : Z,
  Zfast_div_eucl a b = Zdiv_eucl a b.
Proof.
(* Goal: forall a b : Z, @eq (prod Z Z) (Zfast_div_eucl a b) (Z.div_eucl a b) *)
unfold Zfast_div_eucl.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy.
Qed.

End faster_div.

Section Iter.

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

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

Lemma iter_nat_plus :
  forall (p q : nat) (x : A),
  iter_nat (p + q) x = iter_nat p (iter_nat q x).
Proof.
(* Goal: forall (p q : nat) (x : A), @eq A (iter_nat (Init.Nat.add p q) x) (iter_nat p (iter_nat q x)) *)
induction q.
(* Goal: forall x : A, @eq A (iter_nat (Init.Nat.add p O) x) (iter_nat p (iter_nat O x)) *)
(* Goal: forall x : A, @eq A (iter_nat (Init.Nat.add p (S q)) x) (iter_nat p (iter_nat (S q) x)) *)
now rewrite plus_0_r.
(* Goal: forall x : A, @eq A (iter_nat p (f (f x))) (f (iter_nat p (f x))) *)
intros x.
rewrite <- plus_n_Sm.
(* Goal: @eq A (iter_nat (S (Init.Nat.add p q)) x) (iter_nat p (iter_nat (S q) x)) *)
apply IHq.
Qed.

Lemma iter_nat_S :
  forall (p : nat) (x : A),
  iter_nat (S p) x = f (iter_nat p x).
Proof.
(* Goal: forall (p : nat) (x : A), @eq A (iter_nat (S p) x) (f (iter_nat p x)) *)
induction p.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
simpl.
(* Goal: forall x : A, @eq A (iter_nat p (f (f x))) (f (iter_nat p (f x))) *)
intros x.
(* Goal: @eq A (iter_pos p (iter_nat (Pos.to_nat p) x)) (iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) x)) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
apply IHp.
Qed.

Fixpoint iter_pos (n : positive) (x : A) {struct n} : A :=
  match n with
  | xI n' => iter_pos n' (iter_pos n' (f x))
  | xO n' => iter_pos n' (iter_pos n' x)
  | xH => f x
  end.

Lemma iter_pos_nat :
  forall (p : positive) (x : A),
  iter_pos p x = iter_nat (Pos.to_nat p) x.
Proof.
(* Goal: forall x : A, @eq A (iter_nat p (f (f x))) (f (iter_nat p (f x))) *)
induction p ; intros x.
(* Goal: @eq A (iter_pos (xI p) x) (iter_nat (Pos.to_nat (xI p)) x) *)
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Pos.to_nat (xO p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite Pos2Nat.inj_xI.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
simpl.
(* Goal: @eq A (iter_pos p (iter_pos p x)) (iter_nat (Init.Nat.add (Pos.to_nat p) (Init.Nat.add (Pos.to_nat p) O)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite plus_0_r.
(* Goal: @eq A (iter_pos p (iter_pos p x)) (iter_nat (Init.Nat.add (Pos.to_nat p) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite iter_nat_plus.
(* Goal: @eq A (iter_pos p (iter_pos p (f x))) (iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) (f x))) *)
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Pos.to_nat (xO p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite (IHp (f x)).
(* Goal: @eq A (iter_pos p (iter_nat (Pos.to_nat p) x)) (iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) x)) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
apply IHp.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Pos.to_nat (xO p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite Pos2Nat.inj_xO.
(* Goal: @eq A (iter_pos (xO p) x) (iter_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
simpl.
(* Goal: @eq A (iter_pos p (iter_pos p x)) (iter_nat (Init.Nat.add (Pos.to_nat p) (Init.Nat.add (Pos.to_nat p) O)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite plus_0_r.
(* Goal: @eq A (iter_pos p (iter_pos p x)) (iter_nat (Init.Nat.add (Pos.to_nat p) (Pos.to_nat p)) x) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite iter_nat_plus.
(* Goal: @eq A (iter_pos p (iter_pos p x)) (iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) x)) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
rewrite (IHp x).
(* Goal: @eq A (iter_pos p (iter_nat (Pos.to_nat p) x)) (iter_nat (Pos.to_nat p) (iter_nat (Pos.to_nat p) x)) *)
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
apply IHp.
(* Goal: @eq A (iter_pos xH x) (iter_nat (Pos.to_nat xH) x) *)
easy.
Qed.

End Iter.
