Require Import ArithRing.
Require Export ZArith.
Require Export Znumtheory.
Require Export Zpow_facts.



Local Open Scope Z_scope.


Lemma Zlt0_not_eq : forall n, 0<n -> n<>0.

Definition Zdiv_mult_cancel_r a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H).
Definition Zdiv_mult_cancel_l a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H).
Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H).


Hint Extern 2 (Z.le _ _) =>
 (match goal with
   |- Zpos _ <= Zpos _ => exact (eq_refl _)
| H: _ <= ?p |- _ <= ?p => apply Z.le_trans with (2 := H)
| H: _ < ?p |- _ <= ?p => apply Z.lt_le_incl; apply Z.le_lt_trans with (2 := H)
  end).

Hint Extern 2 (Z.lt _ _) =>
 (match goal with
   |- Zpos _ < Zpos _ => exact (eq_refl _)
| H: _ <= ?p |- _ <= ?p => apply Z.lt_le_trans with (2 := H)
| H: _ < ?p |- _ <= ?p => apply Z.le_lt_trans with (2 := H)
  end).

Hint Resolve Z.lt_gt Z.le_ge Z_div_pos: zarith.


 Theorem beta_lex: forall a b c d beta,
       a * beta + b <= c * beta + d ->
       0 <= b < beta -> 0 <= d < beta ->
       a <= c.

 Theorem beta_lex_inv: forall a b c d beta,
      a < c -> 0 <= b < beta ->
      0 <= d < beta ->
      a * beta + b < c * beta + d.

 Lemma beta_mult : forall h l beta,
   0 <= h < beta -> 0 <= l < beta -> 0 <= h*beta+l < beta^2.

 Lemma Zmult_lt_b :
   forall b x y, 0 <= x < b -> 0 <= y < b -> 0 <= x * y <= b^2 - 2*b + 1.

 Lemma sum_mul_carry : forall xh xl yh yl wc cc beta,
   1 < beta ->
   0 <= wc < beta ->
   0 <= xh < beta ->
   0 <= xl < beta ->
   0 <= yh < beta ->
   0 <= yl < beta ->
   0 <= cc < beta^2 ->
   wc*beta^2 + cc = xh*yl + xl*yh ->
   0 <= wc <= 1.

 Theorem mult_add_ineq: forall x y cross beta,
   0 <= x < beta ->
   0 <= y < beta ->
   0 <= cross < beta ->
   0 <= x * y + cross < beta^2.

 Theorem mult_add_ineq2: forall x y c cross beta,
   0 <= x < beta ->
   0 <= y < beta ->
   0 <= c*beta + cross <= 2*beta - 2 ->
   0 <= x * y + (c*beta + cross) < beta^2.

Theorem mult_add_ineq3: forall x y c cross beta,
   0 <= x < beta ->
   0 <= y < beta ->
   0 <= cross <= beta - 2 ->
   0 <= c <= 1 ->
   0 <= x * y + (c*beta + cross) < beta^2.

Hint Rewrite Z.mul_1_r Z.mul_0_r Z.mul_1_l Z.mul_0_l Z.add_0_l Z.add_0_r Z.sub_0_r: rm10.


Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.

 Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
  (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.

 Theorem Zmod_shift_r:
   forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
     (r * 2 ^a + t) mod (2 ^ b) = (r * 2 ^a) mod (2 ^ b) + t.

  Theorem Zdiv_shift_r:
    forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
      (r * 2 ^a + t) / (2 ^ b) = (r * 2 ^a) / (2 ^ b).

 Lemma shift_unshift_mod : forall n p a,
     0 <= a < 2^n ->
     0 <= p <= n ->
     a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n.

 Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n ->
   ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) =
   a mod 2 ^ p.

 Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.

 Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.

 Theorem Zgcd_div_pos a b:
   0 < b -> 0 < Z.gcd a b -> 0 < b / Z.gcd a b.

 Theorem Zdiv_neg a b:
   a < 0 -> 0 < b -> a / b < 0.

 Lemma Zdiv_gcd_zero : forall a b, b / Z.gcd a b = 0 -> b <> 0 ->
  Z.gcd a b = 0.

 Lemma Zgcd_mult_rel_prime : forall a b c,
  Z.gcd a c = 1 -> Z.gcd b c = 1 -> Z.gcd (a*b) c = 1.

 Lemma Zcompare_gt : forall (A:Type)(a a´:A)(p q:Z),
  match (p?=q)%Z with Gt => a | _ => a´ end =
  if Z_le_gt_dec p q then a´ else a.

Theorem Zbounded_induction :
  (forall Q : Z -> Prop, forall b : Z,
    Q 0 ->
    (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
      forall n, 0 <= n -> n < b -> Q n)%Z.

Lemma Zsquare_le x : x <= x*x.