# 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.