# Library Coq.Numbers.BigNumPrelude

# BigNumPrelude

Auxillary functions & theorems used for arbitrary precision efficient numbers.
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.