ZExtra.v

Require Import Coq.ZArith.BinInt.
Require Import Coq.micromega.Lia.
Require Import Coq.ZArith.ZArith.

Local Open Scope Z_scope.

Module ZLib.

Lemma mod2_cases: forall (n: Z), n mod 2 = 0 \/ n mod 2 = 1.forall n : Z, n mod 2 = 0 \/ n mod 2 = 1
Proof.forall n : Z, n mod 2 = 0 \/ n mod 2 = 1
  intros.n:Z
n mod 2 = 0 \/ n mod 2 = 1 pose proof (Z.mod_pos_bound n 2).n:Z
H:0 < 2 -> 0 <= n mod 2 < 2
n mod 2 = 0 \/ n mod 2 = 1 lia.
Qed.

Lemma div_mul_undo: forall a b,
    b <> 0 ->
    a mod b = 0 ->
    a / b * b = a.forall a b : Z, b <> 0 -> a mod b = 0 -> a / b * b = a
Proof.forall a b : Z, b <> 0 -> a mod b = 0 -> a / b * b = a
  intros.a, b:Z
H:b <> 0
H0:a mod b = 0
a / b * b = a
  pose proof Z.div_mul_cancel_l as A.a, b:Z
H:b <> 0
H0:a mod b = 0
A:forall a b c : Z,
b <> 0 -> c <> 0 -> c * a / (c * b) = a / b
a / b * b = a specialize (A a 1 b).a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / (b * 1) = a / 1
a / b * b = a
  replace (b * 1) with b in A by lia.a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a / 1
a / b * b = a
  rewrite Z.div_1_r in A.a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a
a / b * b = a
  rewrite Z.mul_comm.a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a
b * (a / b) = a
  rewrite <- Z.divide_div_mul_exact; try assumption.a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a
b * a / b = a
a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a
(b | a)
  -a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a
b * a / b = a apply A; congruence.
  -a, b:Z
H:b <> 0
H0:a mod b = 0
A:1 <> 0 -> b <> 0 -> b * a / b = a
(b | a) apply Z.mod_divide; assumption.
Qed.

Lemma mod_0_r: forall (m: Z),
    m mod 0 = 0.forall m : Z, m mod 0 = 0
Proof.forall m : Z, m mod 0 = 0
  intros.m:Z
m mod 0 = 0 destruct m; reflexivity.
Qed.

Lemma sub_mod_0: forall (a b m: Z),
    a mod m = 0 ->
    b mod m = 0 ->
    (a - b) mod m = 0.forall a b m : Z,
a mod m = 0 -> b mod m = 0 -> (a - b) mod m = 0
Proof.forall a b m : Z,
a mod m = 0 -> b mod m = 0 -> (a - b) mod m = 0
  intros *.a, b, m:Z
a mod m = 0 -> b mod m = 0 -> (a - b) mod m = 0 intros E1 E2.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(a - b) mod m = 0
  rewrite Zminus_mod.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(a mod m - b mod m) mod m = 0
  rewrite E1.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(0 - b mod m) mod m = 0 rewrite E2.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(0 - 0) mod m = 0
  reflexivity.
Qed.

Lemma add_mod_0: forall a b m : Z,
    a mod m = 0 ->
    b mod m = 0 ->
    (a + b) mod m = 0.forall a b m : Z,
a mod m = 0 -> b mod m = 0 -> (a + b) mod m = 0
Proof.forall a b m : Z,
a mod m = 0 -> b mod m = 0 -> (a + b) mod m = 0
  intros *.a, b, m:Z
a mod m = 0 -> b mod m = 0 -> (a + b) mod m = 0 intros E1 E2.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(a + b) mod m = 0
  rewrite Zplus_mod.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(a mod m + b mod m) mod m = 0
  rewrite E1.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(0 + b mod m) mod m = 0 rewrite E2.a, b, m:Z
E1:a mod m = 0
E2:b mod m = 0
(0 + 0) mod m = 0
  reflexivity.
Qed.

Lemma Z_mod_mult': forall a b : Z,
    (a * b) mod a = 0.forall a b : Z, (a * b) mod a = 0
Proof.forall a b : Z, (a * b) mod a = 0
  intros.a, b:Z
(a * b) mod a = 0 rewrite Z.mul_comm.a, b:Z
(b * a) mod a = 0 apply Z_mod_mult.
Qed.

Lemma mod_add_r: forall a b,
    b <> 0 ->
    (a + b) mod b = a mod b.forall a b : Z, b <> 0 -> (a + b) mod b = a mod b
Proof.forall a b : Z, b <> 0 -> (a + b) mod b = a mod b
  intros.a, b:Z
H:b <> 0
(a + b) mod b = a mod b rewrite <- Z.add_mod_idemp_r by lia.a, b:Z
H:b <> 0
(a + b mod b) mod b = a mod b
  rewrite Z.mod_same by lia.a, b:Z
H:b <> 0
(a + 0) mod b = a mod b
  rewrite Z.add_0_r.a, b:Z
H:b <> 0
a mod b = a mod b
  reflexivity.
Qed.

Lemma mod_pow2_same_cases: forall a n,
    a mod 2 ^ n = a ->
    2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n.forall a n : Z,
a mod 2 ^ n = a ->
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n
Proof.forall a n : Z,
a mod 2 ^ n = a ->
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n
  intros.a, n:Z
H:a mod 2 ^ n = a
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n
  assert (n < 0 \/ 0 <= n) as C by lia.a, n:Z
H:a mod 2 ^ n = a
C:n < 0 \/ 0 <= n
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n destruct C as [C | C].a, n:Z
H:a mod 2 ^ n = a
C:n < 0
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n
a, n:Z
H:a mod 2 ^ n = a
C:0 <= n
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n
  -a, n:Z
H:a mod 2 ^ n = a
C:n < 0
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n left.a, n:Z
H:a mod 2 ^ n = a
C:n < 0
2 ^ n = 0 /\ a = 0 rewrite (Z.pow_neg_r 2 n C) in *.a, n:Z
H:a mod 0 = a
C:n < 0
0 = 0 /\ a = 0 rewrite mod_0_r in H.a, n:Z
H:0 = a
C:n < 0
0 = 0 /\ a = 0 auto.
  -a, n:Z
H:a mod 2 ^ n = a
C:0 <= n
2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n right.a, n:Z
H:a mod 2 ^ n = a
C:0 <= n
0 <= a < 2 ^ n
    rewrite <- H.a, n:Z
H:a mod 2 ^ n = a
C:0 <= n
0 <= a mod 2 ^ n < 2 ^ n apply Z.mod_pos_bound.a, n:Z
H:a mod 2 ^ n = a
C:0 <= n
0 < 2 ^ n
    apply Z.pow_pos_nonneg; lia.
Qed.

Lemma mod_pow2_same_bounds: forall a n,
    a mod 2 ^ n = a ->
    0 <= n ->
    0 <= a < 2 ^ n.forall a n : Z,
a mod 2 ^ n = a -> 0 <= n -> 0 <= a < 2 ^ n
Proof.forall a n : Z,
a mod 2 ^ n = a -> 0 <= n -> 0 <= a < 2 ^ n
  intros.a, n:Z
H:a mod 2 ^ n = a
H0:0 <= n
0 <= a < 2 ^ n rewrite <- H.a, n:Z
H:a mod 2 ^ n = a
H0:0 <= n
0 <= a mod 2 ^ n < 2 ^ n apply Z.mod_pos_bound.a, n:Z
H:a mod 2 ^ n = a
H0:0 <= n
0 < 2 ^ n
  apply Z.pow_pos_nonneg; lia.
Qed.

Lemma pow2_nonneg: forall n,
    0 <= 2 ^ n.forall n : Z, 0 <= 2 ^ n
Proof.forall n : Z, 0 <= 2 ^ n
  intros.n:Z
0 <= 2 ^ n apply Z.pow_nonneg.n:Z
0 <= 2 lia.
Qed.

Lemma pow2_pos: forall n,
    0 <= n ->
    0 < 2 ^ n.forall n : Z, 0 <= n -> 0 < 2 ^ n
Proof.forall n : Z, 0 <= n -> 0 < 2 ^ n
  intros.n:Z
H:0 <= n
0 < 2 ^ n apply Z.pow_pos_nonneg; lia.
Qed.

Lemma pow2_times2: forall i,
    0 < i ->
    2 ^ i = 2 * 2 ^ (i - 1).forall i : Z, 0 < i -> 2 ^ i = 2 * 2 ^ (i - 1)
Proof.forall i : Z, 0 < i -> 2 ^ i = 2 * 2 ^ (i - 1)
  intros.i:Z
H:0 < i
2 ^ i = 2 * 2 ^ (i - 1)
  rewrite <- Z.pow_succ_r by lia.i:Z
H:0 < i
2 ^ i = 2 ^ Z.succ (i - 1)
  f_equal.i:Z
H:0 < i
i = Z.succ (i - 1)
  lia.
Qed.

Lemma pow2_div2: forall i,
    0 <= i ->
    2 ^ (i - 1) = 2 ^ i / 2.forall i : Z, 0 <= i -> 2 ^ (i - 1) = 2 ^ i / 2
Proof.forall i : Z, 0 <= i -> 2 ^ (i - 1) = 2 ^ i / 2
  intros.i:Z
H:0 <= i
2 ^ (i - 1) = 2 ^ i / 2
  assert (i = 0 \/ 0 < i) as C by lia.i:Z
H:0 <= i
C:i = 0 \/ 0 < i
2 ^ (i - 1) = 2 ^ i / 2 destruct C as [C | C].i:Z
H:0 <= i
C:i = 0
2 ^ (i - 1) = 2 ^ i / 2
i:Z
H:0 <= i
C:0 < i
2 ^ (i - 1) = 2 ^ i / 2
  -i:Z
H:0 <= i
C:i = 0
2 ^ (i - 1) = 2 ^ i / 2 subst.H:0 <= 0
2 ^ (0 - 1) = 2 ^ 0 / 2 reflexivity.
  -i:Z
H:0 <= i
C:0 < i
2 ^ (i - 1) = 2 ^ i / 2 rewrite Z.pow_sub_r by lia.i:Z
H:0 <= i
C:0 < i
2 ^ i / 2 ^ 1 = 2 ^ i / 2
    reflexivity.
Qed.

Lemma div_mul_undo_le: forall a b,
    0 <= a ->
    0 < b ->
    a / b * b <= a.forall a b : Z, 0 <= a -> 0 < b -> a / b * b <= a
Proof.forall a b : Z, 0 <= a -> 0 < b -> a / b * b <= a
  intros.a, b:Z
H:0 <= a
H0:0 < b
a / b * b <= a
  pose proof (Zmod_eq_full a b) as P.a, b:Z
H:0 <= a
H0:0 < b
P:b <> 0 -> a mod b = a - a / b * b
a / b * b <= a
  pose proof (Z.mod_bound_pos a b) as Q.a, b:Z
H:0 <= a
H0:0 < b
P:b <> 0 -> a mod b = a - a / b * b
Q:0 <= a -> 0 < b -> 0 <= a mod b < b
a / b * b <= a
  lia.
Qed.

Lemma testbit_true_nonneg: forall a i,
    0 <= a ->
    0 <= i ->
    Z.testbit a i = true ->
    2 ^ i <= a.forall a i : Z,
0 <= a -> 0 <= i -> Z.testbit a i = true -> 2 ^ i <= a
Proof.forall a i : Z,
0 <= a -> 0 <= i -> Z.testbit a i = true -> 2 ^ i <= a
  intros.a, i:Z
H:0 <= a
H0:0 <= i
H1:Z.testbit a i = true
2 ^ i <= a
  apply Z.testbit_true in H1; [|assumption].a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
2 ^ i <= a
  pose proof (pow2_pos i H0).a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
2 ^ i <= a
  eapply Z.le_trans; [| apply (div_mul_undo_le a (2 ^ i)); lia].a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
2 ^ i <= a / 2 ^ i * 2 ^ i
  replace (2 ^ i) with (1 * 2 ^ i) at 1 by lia.a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
1 * 2 ^ i <= a / 2 ^ i * 2 ^ i
  apply Z.mul_le_mono_nonneg_r; [lia|].a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
1 <= a / 2 ^ i
  pose proof (Z.div_pos a (2 ^ i)).a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
H3:0 <= a -> 0 < 2 ^ i -> 0 <= a / 2 ^ i
1 <= a / 2 ^ i
  assert (a / 2 ^ i <> 0); [|lia].a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
H3:0 <= a -> 0 < 2 ^ i -> 0 <= a / 2 ^ i
a / 2 ^ i <> 0
  intro E.a, i:Z
H:0 <= a
H0:0 <= i
H1:(a / 2 ^ i) mod 2 = 1
H2:0 < 2 ^ i
H3:0 <= a -> 0 < 2 ^ i -> 0 <= a / 2 ^ i
E:a / 2 ^ i = 0
False rewrite E in H1.a, i:Z
H:0 <= a
H0:0 <= i
H1:0 mod 2 = 1
H2:0 < 2 ^ i
H3:0 <= a -> 0 < 2 ^ i -> 0 <= a / 2 ^ i
E:a / 2 ^ i = 0
False cbv in H1.a, i:Z
H:0 <= a
H0:0 <= i
H1:0 = 1
H2:0 < 2 ^ i
H3:0 <= a -> 0 < 2 ^ i -> 0 <= a / 2 ^ i
E:a / 2 ^ i = 0
False discriminate H1.
Qed.

Lemma range_div_pos: forall a b c d,
    0 < d ->
    a <= b <= c ->
    a / d <= b / d <= c / d.forall a b c d : Z,
0 < d -> a <= b <= c -> a / d <= b / d <= c / d
Proof.forall a b c d : Z,
0 < d -> a <= b <= c -> a / d <= b / d <= c / d
  intuition idtac.a, b, c, d:Z
H:0 < d
H1:a <= b
H2:b <= c
a / d <= b / d
a, b, c, d:Z
H:0 < d
H1:a <= b
H2:b <= c
b / d <= c / d
  -a, b, c, d:Z
H:0 < d
H1:a <= b
H2:b <= c
a / d <= b / d apply (Z.div_le_mono _ _ _ H H1).
  -a, b, c, d:Z
H:0 < d
H1:a <= b
H2:b <= c
b / d <= c / d apply (Z.div_le_mono _ _ _ H H2).
Qed.

Lemma testbit_true_nonneg': forall a i,
    0 <= i ->
    2 ^ i <= a < 2 ^ (i + 1) ->
    Z.testbit a i = true.forall a i : Z,
0 <= i ->
2 ^ i <= a < 2 ^ (i + 1) -> Z.testbit a i = true
Proof.forall a i : Z,
0 <= i ->
2 ^ i <= a < 2 ^ (i + 1) -> Z.testbit a i = true
  intros.a, i:Z
H:0 <= i
H0:2 ^ i <= a < 2 ^ (i + 1)
Z.testbit a i = true
  apply Z.testbit_true; [assumption|].a, i:Z
H:0 <= i
H0:2 ^ i <= a < 2 ^ (i + 1)
(a / 2 ^ i) mod 2 = 1
  destruct H0 as [A B].a, i:Z
H:0 <= i
A:2 ^ i <= a
B:a < 2 ^ (i + 1)
(a / 2 ^ i) mod 2 = 1
  pose proof (pow2_pos i H) as Q.a, i:Z
H:0 <= i
A:2 ^ i <= a
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
(a / 2 ^ i) mod 2 = 1
  apply (Z.div_le_mono _ _ _ Q) in A.a, i:Z
H:0 <= i
A:2 ^ i / 2 ^ i <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
(a / 2 ^ i) mod 2 = 1
  rewrite Z_div_same in A by lia.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
(a / 2 ^ i) mod 2 = 1
  pose proof (Z.div_lt_upper_bound a (2 ^ i) 2 Q) as P.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a < 2 ^ i * 2 -> a / 2 ^ i < 2
(a / 2 ^ i) mod 2 = 1
  rewrite Z.mul_comm in P.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a < 2 * 2 ^ i -> a / 2 ^ i < 2
(a / 2 ^ i) mod 2 = 1
  replace i with (i + 1 - 1) in P by lia.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a < 2 * 2 ^ (i + 1 - 1) -> a / 2 ^ (i + 1 - 1) < 2
(a / 2 ^ i) mod 2 = 1
  rewrite <- pow2_times2 in P by lia.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a < 2 ^ (i + 1) -> a / 2 ^ (i + 1 - 1) < 2
(a / 2 ^ i) mod 2 = 1
  specialize (P B).a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a / 2 ^ (i + 1 - 1) < 2
(a / 2 ^ i) mod 2 = 1
  replace (i + 1 - 1) with i in P by lia.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a / 2 ^ i < 2
(a / 2 ^ i) mod 2 = 1
  replace (a / 2 ^ i) with 1 by lia.a, i:Z
H:0 <= i
A:1 <= a / 2 ^ i
B:a < 2 ^ (i + 1)
Q:0 < 2 ^ i
P:a / 2 ^ i < 2
1 mod 2 = 1
  reflexivity.
Qed.

Lemma testbit_false_nonneg: forall a i,
    0 <= a < 2 ^ i ->
    0 < i ->
    Z.testbit a (i - 1) = false ->
    a < 2 ^ (i - 1).forall a i : Z,
0 <= a < 2 ^ i ->
0 < i ->
Z.testbit a (i - 1) = false -> a < 2 ^ (i - 1)
Proof.forall a i : Z,
0 <= a < 2 ^ i ->
0 < i ->
Z.testbit a (i - 1) = false -> a < 2 ^ (i - 1)
  intros.a, i:Z
H:0 <= a < 2 ^ i
H0:0 < i
H1:Z.testbit a (i - 1) = false
a < 2 ^ (i - 1)
  assert (2 ^ (i - 1) <= a < 2 ^ i \/ a < 2 ^ (i - 1)) as C by lia.a, i:Z
H:0 <= a < 2 ^ i
H0:0 < i
H1:Z.testbit a (i - 1) = false
C:2 ^ (i - 1) <= a < 2 ^ i \/ a < 2 ^ (i - 1)
a < 2 ^ (i - 1)
  destruct C as [C | C]; [exfalso|assumption].a, i:Z
H:0 <= a < 2 ^ i
H0:0 < i
H1:Z.testbit a (i - 1) = false
C:2 ^ (i - 1) <= a < 2 ^ i
False
  assert (Z.testbit a (i - 1) = true); [|congruence].a, i:Z
H:0 <= a < 2 ^ i
H0:0 < i
H1:Z.testbit a (i - 1) = false
C:2 ^ (i - 1) <= a < 2 ^ i
Z.testbit a (i - 1) = true
  replace i with (i - 1 + 1) in C at 2 by lia.a, i:Z
H:0 <= a < 2 ^ i
H0:0 < i
H1:Z.testbit a (i - 1) = false
C:2 ^ (i - 1) <= a < 2 ^ (i - 1 + 1)
Z.testbit a (i - 1) = true
  apply testbit_true_nonneg'; lia.
Qed.

Lemma signed_bounds_to_sz_pos: forall sz n,
    - 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) ->
    0 < sz.forall sz n : Z,
- 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) -> 0 < sz
Proof.forall sz n : Z,
- 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) -> 0 < sz
  intros.sz, n:Z
H:- 2 ^ (sz - 1) <= n < 2 ^ (sz - 1)
0 < sz
  assert (0 < sz \/ sz - 1 < 0) as C by lia.sz, n:Z
H:- 2 ^ (sz - 1) <= n < 2 ^ (sz - 1)
C:0 < sz \/ sz - 1 < 0
0 < sz
  destruct C as [C | C]; [assumption|exfalso].sz, n:Z
H:- 2 ^ (sz - 1) <= n < 2 ^ (sz - 1)
C:sz - 1 < 0
False
  rewrite Z.pow_neg_r in H by assumption.sz, n:Z
H:- 0 <= n < 0
C:sz - 1 < 0
False
  lia.
Qed.

Lemma two_digits_encoding_inj_lo: forall base a b c d: Z,
  0 <= b < base ->
  0 <= d < base ->
  base * a + b = base * c + d ->
  b = d.forall base a b c d : Z,
0 <= b < base ->
0 <= d < base -> base * a + b = base * c + d -> b = d
Proof.forall base a b c d : Z,
0 <= b < base ->
0 <= d < base -> base * a + b = base * c + d -> b = d
  intros.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
b = d
  pose proof Z.mod_unique as P.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:forall a b q r : Z,
0 <= r < b \/ b < r <= 0 ->
a = b * q + r -> r = a mod b
b = d
  specialize P with (b := base) (q := c) (r := d).base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:forall a : Z,
0 <= d < base \/ base < d <= 0 ->
a = base * c + d -> d = a mod base
b = d
  specialize P with (2 := H1).base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = d
  rewrite P by lia.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = (base * a + b) mod base
  rewrite <- Z.add_mod_idemp_l by lia.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = ((base * a) mod base + b) mod base
  rewrite Z.mul_comm.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = ((a * base) mod base + b) mod base
  rewrite Z.mod_mul by lia.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = (0 + b) mod base
  rewrite Z.add_0_l.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = b mod base
  rewrite Z.mod_small by lia.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
P:0 <= d < base \/ base < d <= 0 ->
d = (base * a + b) mod base
b = b
  reflexivity.
Qed.

Lemma two_digits_encoding_inj_hi: forall base a b c d: Z,
  0 <= b < base ->
  0 <= d < base ->
  base * a + b = base * c + d ->
  a = c.forall base a b c d : Z,
0 <= b < base ->
0 <= d < base -> base * a + b = base * c + d -> a = c
Proof.forall base a b c d : Z,
0 <= b < base ->
0 <= d < base -> base * a + b = base * c + d -> a = c
  intros.base, a, b, c, d:Z
H:0 <= b < base
H0:0 <= d < base
H1:base * a + b = base * c + d
a = c nia.
Qed.

Lemma Z_to_nat_neg: forall (n: Z),
    n < 0 ->
    Z.to_nat n = 0%nat.forall n : Z, n < 0 -> Z.to_nat n = 0%nat
Proof.forall n : Z, n < 0 -> Z.to_nat n = 0%nat
  intros.n:Z
H:n < 0
Z.to_nat n = 0%nat destruct n; (lia||reflexivity).
Qed.

End ZLib.

Module ZExtra.

  Lemma mod_0_bounds :
    forall x y m,
      0 < m ->
      x mod m = 0 ->
      y mod m = 0 ->
      x <> y ->
      x + m > y ->
      y + m <= x.forall x y m : Z,
0 < m ->
x mod m = 0 ->
y mod m = 0 -> x <> y -> x + m > y -> y + m <= x
  Proof.forall x y m : Z,
0 < m ->
x mod m = 0 ->
y mod m = 0 -> x <> y -> x + m > y -> y + m <= x
    intros x y m.x, y, m:Z
0 < m ->
x mod m = 0 ->
y mod m = 0 -> x <> y -> x + m > y -> y + m <= x
    intros POS XMOD YMOD NEQ H.x, y, m:Z
POS:0 < m
XMOD:x mod m = 0
YMOD:y mod m = 0
NEQ:x <> y
H:x + m > y
y + m <= x
    destruct (Z_le_gt_dec (y + m) x); eauto.x, y, m:Z
POS:0 < m
XMOD:x mod m = 0
YMOD:y mod m = 0
NEQ:x <> y
H:x + m > y
g:y + m > x
y + m <= x

    apply Znumtheory.Zmod_divide in YMOD; try lia.x, y, m:Z
POS:0 < m
XMOD:x mod m = 0
YMOD:(m | y)
NEQ:x <> y
H:x + m > y
g:y + m > x
y + m <= x
    apply Znumtheory.Zmod_divide in XMOD; try lia.x, y, m:Z
POS:0 < m
XMOD:(m | x)
YMOD:(m | y)
NEQ:x <> y
H:x + m > y
g:y + m > x
y + m <= x
    inversion XMOD as [x']; subst; clear XMOD.y, m:Z
POS:0 < m
x':Z
YMOD:(m | y)
g:y + m > x' * m
H:x' * m + m > y
NEQ:x' * m <> y
y + m <= x' * m
    inversion YMOD as [y']; subst; clear YMOD.m:Z
POS:0 < m
x', y':Z
NEQ:x' * m <> y' * m
H:x' * m + m > y' * m
g:y' * m + m > x' * m
y' * m + m <= x' * m

    assert (x' <> y') as NEQ' by lia; clear NEQ.m:Z
POS:0 < m
x', y':Z
H:x' * m + m > y' * m
g:y' * m + m > x' * m
NEQ':x' <> y'
y' * m + m <= x' * m

    rewrite <- Z.mul_succ_l in H.m:Z
POS:0 < m
x', y':Z
H:Z.succ x' * m > y' * m
g:y' * m + m > x' * m
NEQ':x' <> y'
y' * m + m <= x' * m
    rewrite <- Z.mul_succ_l in g.m:Z
POS:0 < m
x', y':Z
H:Z.succ x' * m > y' * m
g:Z.succ y' * m > x' * m
NEQ':x' <> y'
y' * m + m <= x' * m
    apply Zmult_gt_reg_r in H;
      apply Zmult_gt_reg_r in g; lia.
  Qed.

  Lemma Ple_not_eq :
    forall x y,
    (x < y)%positive -> x <> y.forall x y : positive, (x < y)%positive -> x <> y
  Proof.forall x y : positive, (x < y)%positive -> x <> y lia. Qed.

  Lemma Pge_not_eq :
    forall x y,
    (y < x)%positive -> x <> y.forall x y : positive, (y < x)%positive -> x <> y
  Proof.forall x y : positive, (y < x)%positive -> x <> y lia. Qed.

  Lemma Ple_Plt_Succ :
    forall x y n,
    (x <= y)%positive -> (x < y + n)%positive.forall x y n : positive,
(x <= y)%positive -> (x < y + n)%positive
  Proof.forall x y n : positive,
(x <= y)%positive -> (x < y + n)%positive lia. Qed.

End ZExtra.