Library compcert.flocq.Core.Fcore_Zaux

Require Import ZArith.
Require Import Zquot.

Section Zmissing.

Theorem Zopp_le_cancel :
  ∀ x y : Z,
  (-y ≤ -x)%Z → Zle x y.
Proof.
intros x y Hxy.
apply Zplus_le_reg_r with (-x - y)%Z.
now ring_simplify.
Qed.

Theorem Zgt_not_eq :
  ∀ x y : Z,
  (y < x)%Z → (x ≠ y)%Z.
Proof.
intros x y H Hn.
apply Zlt_irrefl with 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 : ∀ (b : bool) (h1 h2 : b = true), h1 = h2.
Proof.
assert (∀ (h : true = true), refl_equal true = h).
apply (eq_dep_elim bool true (eqbool_dep _ _) (refl_equal _)).
intros b.
case b.
intros h1 h2.
now rewrite <- (H h1).
intros h.
discriminate h.
Qed.

End Proof_Irrelevance.

Section Even_Odd.

Definition Zeven (n : Z) :=
  match n with
  | Zpos (xO _) ⇒ true
  | Zneg (xO _) ⇒ true
  | Z0 ⇒ true
  | _ ⇒ false
  end.

Theorem Zeven_mult :
  ∀ x y, Zeven (x × y) = orb (Zeven x) (Zeven y).
Proof.
now intros [|[xp|xp|]|[xp|xp|]] [|[yp|yp|]|[yp|yp|]].
Qed.

Theorem Zeven_opp :
  ∀ x, Zeven (- x) = Zeven x.
Proof.
now intros [|[n|n|]|[n|n|]].
Qed.

Theorem Zeven_ex :
  ∀ x, ∃ p, x = (2 × p + if Zeven x then 0 else 1)%Z.
Proof.
intros [|[n|n|]|[n|n|]].
now ∃ Z0.
now ∃ (Zpos n).
now ∃ (Zpos n).
now ∃ Z0.
∃ (Zneg n - 1)%Z.
change (2 × Zneg n - 1 = 2 × (Zneg n - 1) + 1)%Z.
ring.
now ∃ (Zneg n).
now ∃ (-1)%Z.
Qed.

Theorem Zeven_2xp1 :
  ∀ n, Zeven (2 × n + 1) = false.
Proof.
intros n.
destruct (Zeven_ex (2 × n + 1)) as (p, Hp).
revert Hp.
case (Zeven (2 × n + 1)) ; try easy.
intros H.
apply False_ind.
omega.
Qed.

Theorem Zeven_plus :
  ∀ x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).
Proof.
intros x y.
destruct (Zeven_ex x) as (px, Hx).
rewrite Hx at 1.
destruct (Zeven_ex y) as (py, Hy).
rewrite Hy at 1.
replace (2 × px + (if Zeven x then 0 else 1) + (2 × py + (if Zeven y then 0 else 1)))%Z
  with (2 × (px + py) + ((if Zeven x then 0 else 1) + (if Zeven y then 0 else 1)))%Z by ring.
case (Zeven x) ; case (Zeven y).
rewrite Zplus_0_r.
now rewrite Zeven_mult.
apply Zeven_2xp1.
apply Zeven_2xp1.
replace (2 × (px + py) + (1 + 1))%Z with (2 × (px + py + 1))%Z by ring.
now rewrite Zeven_mult.
Qed.

End Even_Odd.

Section Zpower.

Theorem Zpower_plus :
  ∀ n k1 k2, (0 ≤ k1)%Z → (0 ≤ k2)%Z →
  Zpower n (k1 + k2) = (Zpower n k1 × Zpower n k2)%Z.
Proof.
intros n k1 k2 H1 H2.
now apply Zpower_exp ; apply Zle_ge.
Qed.

Theorem Zpower_Zpower_nat :
  ∀ b e, (0 ≤ e)%Z →
  Zpower b e = Zpower_nat b (Zabs_nat e).
Proof.
intros b [|e|e] He.
apply refl_equal.
apply Zpower_pos_nat.
elim He.
apply refl_equal.
Qed.

Theorem Zpower_nat_S :
  ∀ b e,
  Zpower_nat b (S e) = (b × Zpower_nat b e)%Z.
Proof.
intros b e.
rewrite (Zpower_nat_is_exp 1 e).
apply (f_equal (fun x ⇒ x × _)%Z).
apply Zmult_1_r.
Qed.

Theorem Zpower_pos_gt_0 :
  ∀ b p, (0 < b)%Z →
  (0 < Zpower_pos b p)%Z.
Proof.
intros b p Hb.
rewrite Zpower_pos_nat.
induction (nat_of_P p).
easy.
rewrite Zpower_nat_S.
now apply Zmult_lt_0_compat.
Qed.

Theorem Zeven_Zpower :
  ∀ b e, (0 < e)%Z →
  Zeven (Zpower b e) = Zeven b.
Proof.
intros b e He.
case_eq (Zeven b) ; intros Hb.
replace e with (e - 1 + 1)%Z by ring.
rewrite Zpower_exp.
rewrite Zeven_mult.
replace (Zeven (b ^ 1)) with true.
apply Bool.orb_true_r.
unfold Zpower, Zpower_pos. simpl.
now rewrite Zmult_1_r.
omega.
discriminate.
rewrite Zpower_Zpower_nat.
induction (Zabs_nat e).
easy.
unfold Zpower_nat. simpl.
rewrite Zeven_mult.
now rewrite Hb.
now apply Zlt_le_weak.
Qed.

Theorem Zeven_Zpower_odd :
  ∀ b e, (0 ≤ e)%Z → Zeven b = false →
  Zeven (Zpower b e) = false.
Proof.
intros b e He Hb.
destruct (Z_le_lt_eq_dec _ _ He) as [He'|He'].
rewrite <- Hb.
now apply Zeven_Zpower.
now rewrite <- He'.
Qed.

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

Theorem radix_val_inj :
  ∀ r1 r2, radix_val r1 = radix_val r2 → r1 = r2.
Proof.
intros (r1, H1) (r2, H2) H.
simpl in H.
revert H1.
rewrite H.
intros H1.
apply f_equal.
apply eqbool_irrelevance.
Qed.

Definition radix2 := Build_radix 2 (refl_equal _).

Variable r : radix.

Theorem radix_gt_0 : (0 < r)%Z.
Proof.
apply Zlt_le_trans with 2%Z.
easy.
apply Zle_bool_imp_le.
apply r.
Qed.

Theorem radix_gt_1 : (1 < r)%Z.
Proof.
destruct r as (v, Hr). simpl.
apply Zlt_le_trans with 2%Z.
easy.
now apply Zle_bool_imp_le.
Qed.

Theorem Zpower_gt_1 :
  ∀ p,
  (0 < p)%Z →
  (1 < Zpower r p)%Z.
Proof.
intros [|p|p] Hp ; try easy.
simpl.
rewrite Zpower_pos_nat.
generalize (lt_O_nat_of_P p).
induction (nat_of_P p).
easy.
intros _.
rewrite Zpower_nat_S.
assert (0 < Zpower_nat r n)%Z.
clear.
induction n.
easy.
rewrite Zpower_nat_S.
apply Zmult_lt_0_compat with (2 := IHn).
apply radix_gt_0.
apply Zle_lt_trans with (1 × Zpower_nat r n)%Z.
rewrite Zmult_1_l.
now apply (Zlt_le_succ 0).
apply Zmult_lt_compat_r with (1 := H).
apply radix_gt_1.
Qed.

Theorem Zpower_gt_0 :
  ∀ p,
  (0 ≤ p)%Z →
  (0 < Zpower r p)%Z.
Proof.
intros p Hp.
rewrite Zpower_Zpower_nat with (1 := Hp).
induction (Zabs_nat p).
easy.
rewrite Zpower_nat_S.
apply Zmult_lt_0_compat with (2 := IHn).
apply radix_gt_0.
Qed.

Theorem Zpower_ge_0 :
  ∀ e,
  (0 ≤ Zpower r e)%Z.
Proof.
intros [|e|e] ; try easy.
apply Zlt_le_weak.
now apply Zpower_gt_0.
Qed.

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

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

Theorem Zpower_lt_Zpower :
  ∀ e1 e2,
  (Zpower r (e1 - 1) < Zpower r e2)%Z →
  (e1 ≤ e2)%Z.
Proof.
intros e1 e2 He.
apply Znot_gt_le.
intros H.
apply Zlt_not_le with (1 := He).
apply Zpower_le.
clear -H ; omega.
Qed.

End Zpower.

Section Div_Mod.

Theorem Zmod_mod_mult :
  ∀ n a b, (0 < a)%Z → (0 ≤ b)%Z →
  Zmod (Zmod n (a × b)) b = Zmod n b.
Proof.
intros n a [|b|b] Ha Hb.
now rewrite 2!Zmod_0_r.
rewrite (Zmod_eq n (a × Zpos b)).
rewrite Zmult_assoc.
unfold Zminus.
rewrite Zopp_mult_distr_l.
apply Z_mod_plus.
easy.
apply Zmult_gt_0_compat.
now apply Zlt_gt.
easy.
now elim Hb.
Qed.

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

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

Theorem Zdiv_mod_mult :
  ∀ n a b, (0 ≤ a)%Z → (0 ≤ b)%Z →
  (Zdiv (Zmod n (a × b)) a) = Zmod (Zdiv n a) b.
Proof.
intros n a b Ha Hb.
destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].
destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|Hb'].
rewrite (Zmod_eq n (a × b)).
rewrite (Zmult_comm a b) at 2.
rewrite Zmult_assoc.
unfold Zminus.
rewrite Zopp_mult_distr_l.
rewrite Z_div_plus by now apply Zlt_gt.
rewrite <- Zdiv_Zdiv by easy.
apply sym_eq.
apply Zmod_eq.
now apply Zlt_gt.
now apply Zmult_gt_0_compat ; apply Zlt_gt.
rewrite <- Hb'.
rewrite Zmult_0_r, 2!Zmod_0_r.
apply Zdiv_0_l.
rewrite <- Ha'.
now rewrite 2!Zdiv_0_r, Zmod_0_l.
Qed.

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

Theorem ZOdiv_small_abs :
  ∀ a b,
  (Zabs a < b)%Z → Z.quot a b = Z0.
Proof.
intros a b Ha.
destruct (Zle_or_lt 0 a) as [H|H].
apply Zquot_small.
split.
exact H.
now rewrite Zabs_eq in Ha.
apply Zopp_inj.
rewrite <- Zquot_opp_l, Zopp_0.
apply Zquot_small.
generalize (Zabs_non_eq a).
omega.
Qed.

Theorem ZOmod_small_abs :
  ∀ a b,
  (Zabs a < b)%Z → Z.rem a b = a.
Proof.
intros a b Ha.
destruct (Zle_or_lt 0 a) as [H|H].
apply Zrem_small.
split.
exact H.
now rewrite Zabs_eq in Ha.
apply Zopp_inj.
rewrite <- Zrem_opp_l.
apply Zrem_small.
generalize (Zabs_non_eq a).
omega.
Qed.

Theorem ZOdiv_plus :
  ∀ 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.
intros a b c Hab.
destruct (Z_eq_dec c 0) as [Zc|Zc].
now rewrite Zc, 4!Zquot_0_r.
apply Zmult_reg_r with (1 := Zc).
rewrite 2!Zmult_plus_distr_l.
assert (∀ d, Z.quot d c × c = d - Z.rem d c)%Z.
intros d.
rewrite ZOmod_eq.
ring.
rewrite 4!H.
rewrite <- Zplus_rem with (1 := Hab).
ring.
Qed.

End Div_Mod.

Section Same_sign.

Theorem Zsame_sign_trans :
  ∀ v u w, v ≠ Z0 →
  (0 ≤ u × v)%Z → (0 ≤ v × w)%Z → (0 ≤ u × w)%Z.
Proof.
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now elim Zv.
Qed.

Theorem Zsame_sign_trans_weak :
  ∀ v u w, (v = Z0 → w = Z0) →
  (0 ≤ u × v)%Z → (0 ≤ v × w)%Z → (0 ≤ u × w)%Z.
Proof.
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now discriminate Zv.
Qed.

Theorem Zsame_sign_imp :
  ∀ u v,
  (0 < u → 0 ≤ v)%Z →
  (0 < -u → 0 ≤ -v)%Z →
  (0 ≤ u × v)%Z.
Proof.
intros [|u|u] v Hp Hn.
easy.
apply Zmult_le_0_compat.
easy.
now apply Hp.
replace (Zneg u × v)%Z with (Zpos u × (-v))%Z.
apply Zmult_le_0_compat.
easy.
now apply Hn.
rewrite <- Zopp_mult_distr_r.
apply Zopp_mult_distr_l.
Qed.

Theorem Zsame_sign_odiv :
  ∀ u v, (0 ≤ v)%Z →
  (0 ≤ u × Z.quot u v)%Z.
Proof.
intros u v Hv.
apply Zsame_sign_imp ; intros Hu.
apply Z_quot_pos with (2 := Hv).
now apply Zlt_le_weak.
rewrite <- Zquot_opp_l.
apply Z_quot_pos with (2 := Hv).
now apply Zlt_le_weak.
Qed.

End Same_sign.

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 :
  ∀ x y, Zeq_bool_prop x y (Zeq_bool x y).
Proof.
intros x y.
generalize (Zeq_is_eq_bool x y).
case (Zeq_bool x y) ; intros (H1, H2) ; constructor.
now apply H2.
intros H.
specialize (H1 H).
discriminate H1.
Qed.

Theorem Zeq_bool_true :
  ∀ x y, x = y → Zeq_bool x y = true.
Proof.
intros x y.
apply → Zeq_is_eq_bool.
Qed.

Theorem Zeq_bool_false :
  ∀ x y, x ≠ y → Zeq_bool x y = false.
Proof.
intros x y.
generalize (proj2 (Zeq_is_eq_bool x y)).
case Zeq_bool.
intros He Hn.
elim Hn.
now apply He.
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 :
  ∀ x y, Zle_bool_prop x y (Zle_bool x y).
Proof.
intros x y.
generalize (Zle_is_le_bool x y).
case Zle_bool ; intros (H1, H2) ; constructor.
now apply H2.
destruct (Zle_or_lt x y) as [H|H].
now specialize (H1 H).
exact H.
Qed.

Theorem Zle_bool_true :
  ∀ x y : Z,
  (x ≤ y)%Z → Zle_bool x y = true.
Proof.
intros x y.
apply (proj1 (Zle_is_le_bool x y)).
Qed.

Theorem Zle_bool_false :
  ∀ x y : Z,
  (y < x)%Z → Zle_bool x y = false.
Proof.
intros x y Hxy.
generalize (Zle_cases x y).
case Zle_bool ; intros H.
elim (Zlt_irrefl x).
now apply Zle_lt_trans with y.
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 :
  ∀ x y, Zlt_bool_prop x y (Zlt_bool x y).
Proof.
intros x y.
generalize (Zlt_is_lt_bool x y).
case Zlt_bool ; intros (H1, H2) ; constructor.
now apply H2.
destruct (Zle_or_lt y x) as [H|H].
exact H.
now specialize (H1 H).
Qed.

Theorem Zlt_bool_true :
  ∀ x y : Z,
  (x < y)%Z → Zlt_bool x y = true.
Proof.
intros x y.
apply (proj1 (Zlt_is_lt_bool x y)).
Qed.

Theorem Zlt_bool_false :
  ∀ x y : Z,
  (y ≤ x)%Z → Zlt_bool x y = false.
Proof.
intros x y Hxy.
generalize (Zlt_cases x y).
case Zlt_bool ; intros H.
elim (Zlt_irrefl x).
now apply Zlt_le_trans with y.
apply refl_equal.
Qed.

Theorem negb_Zle_bool :
  ∀ x y : Z,
  negb (Zle_bool x y) = Zlt_bool y x.
Proof.
intros x y.
case Zle_bool_spec ; intros H.
now rewrite Zlt_bool_false.
now rewrite Zlt_bool_true.
Qed.

Theorem negb_Zlt_bool :
  ∀ x y : Z,
  negb (Zlt_bool x y) = Zle_bool y x.
Proof.
intros x y.
case Zlt_bool_spec ; intros H.
now rewrite Zle_bool_false.
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 :
  ∀ x y, Zcompare_prop x y (Zcompare x y).
Proof.
intros x y.
destruct (Z_dec x y) as [[H|H]|H].
generalize (Zlt_compare _ _ H).
case (Zcompare x y) ; try easy.
now constructor.
generalize (Zgt_compare _ _ H).
case (Zcompare x y) ; try easy.
constructor.
now apply Zgt_lt.
generalize (proj2 (Zcompare_Eq_iff_eq _ _) H).
case (Zcompare x y) ; try easy.
now constructor.
Qed.

Theorem Zcompare_Lt :
  ∀ x y,
  (x < y)%Z → Zcompare x y = Lt.
Proof.
easy.
Qed.

Theorem Zcompare_Eq :
  ∀ x y,
  (x = y)%Z → Zcompare x y = Eq.
Proof.
intros x y.
apply <- Zcompare_Eq_iff_eq.
Qed.

Theorem Zcompare_Gt :
  ∀ x y,
  (y < x)%Z → Zcompare x y = Gt.
Proof.
intros x y.
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 :
  ∀ b m,
  Zabs (cond_Zopp b m) = Zabs m.
Proof.
intros [|] m.
apply Zabs_Zopp.
apply refl_equal.
Qed.

Theorem cond_Zopp_Zlt_bool :
  ∀ m,
  cond_Zopp (Zlt_bool m 0) m = Zabs m.
Proof.
intros m.
apply sym_eq.
case Zlt_bool_spec ; intros Hm.
apply Zabs_non_eq.
now apply Zlt_le_weak.
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 :
  ∀ v e, Zfast_pow_pos v e = Zpower_pos v e.
Proof.
intros v e.
rewrite <- (Zmult_1_r (Zfast_pow_pos v e)).
unfold Z.pow_pos.
generalize 1%Z.
revert v.
induction e ; intros v f ; simpl.
- rewrite <- 2!IHe.
  rewrite Z.square_spec.
  ring.
- rewrite <- 2!IHe.
  rewrite Z.square_spec.
  apply eq_sym, Zmult_assoc.
- apply eq_refl.
Qed.

End fast_pow_pos.

Section faster_div.

Lemma Zdiv_eucl_unique :
  ∀ a b,
  Zdiv_eucl a b = (Zdiv a b, Zmod a b).
Proof.
intros a b.
unfold Zdiv, Zmod.
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 :
  ∀ a b,
  Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Zpos b).
Proof.
intros a b.
revert a.
induction b ; intros a.
- easy.
- change (Z.pos_div_eucl a (Zpos b~0)) with (Zdiv_eucl (Zpos a) (Zpos b~0)).
  rewrite Zdiv_eucl_unique.
  change (Zpos b~0) with (2 × Zpos b)%Z.
  rewrite Z.rem_mul_r by easy.
  rewrite <- Zdiv_Zdiv by easy.
  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).
    rewrite IHb. clear IHb.
    change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
    rewrite Zdiv_eucl_unique.
    change (Zpos a~1) with (1 + 2 × Zpos a)%Z.
    rewrite (Zmult_comm 2 (Zpos a)).
    rewrite Z_div_plus_full by easy.
    apply f_equal.
    rewrite Z_mod_plus_full.
    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).
    rewrite IHb. clear IHb.
    change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
    rewrite Zdiv_eucl_unique.
    change (Zpos a~0) with (2 × Zpos a)%Z.
    rewrite (Zmult_comm 2 (Zpos a)).
    rewrite Z_div_mult_full by easy.
    apply f_equal.
    now rewrite Z_mod_mult.
  + easy.
- change (Z.pos_div_eucl a 1) with (Zdiv_eucl (Zpos a) 1).
  rewrite Zdiv_eucl_unique.
  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 :
  ∀ a b,
  Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Zpos b).
Proof.
intros a b.
unfold Zpos_div_eucl_aux.
change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
rewrite Zdiv_eucl_unique.
case Pos.compare_spec ; intros H.
now rewrite H, Z_div_same, Z_mod_same.
now rewrite Zdiv_small, Zmod_small by (split ; easy).
rewrite Zpos_div_eucl_aux1_correct.
change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (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 :
  ∀ a b : Z,
  Zfast_div_eucl a b = Zdiv_eucl a b.
Proof.
unfold Zfast_div_eucl.
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 :
  ∀ (p q : nat) (x : A),
  iter_nat (p + q) x = iter_nat p (iter_nat q x).
Proof.
induction q.
now rewrite plus_0_r.
intros x.
rewrite <- plus_n_Sm.
apply IHq.
Qed.

Lemma iter_nat_S :
  ∀ (p : nat) (x : A),
  iter_nat (S p) x = f (iter_nat p x).
Proof.
induction p.
easy.
simpl.
intros 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 :
  ∀ (p : positive) (x : A),
  iter_pos p x = iter_nat (Pos.to_nat p) x.
Proof.
induction p ; intros x.
rewrite Pos2Nat.inj_xI.
simpl.
rewrite plus_0_r.
rewrite iter_nat_plus.
rewrite (IHp (f x)).
apply IHp.
rewrite Pos2Nat.inj_xO.
simpl.
rewrite plus_0_r.
rewrite iter_nat_plus.
rewrite (IHp x).
apply IHp.
easy.
Qed.

End Iter.