Library Stdlib.ZArith.Zdivisibility
From Stdlib Require Import BinInt Wf_Z ZArithRing Zdiv Lia.
Module Z.
Local Open Scope Z_scope.
Lemma mod0_divide : forall a b, (b | a) -> a mod b = 0.
Lemma absle_divide a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.
Lemma BoolSpec_divide_nz a b (H : a <> 0) : BoolSpec (Z.divide a b) (~ Z.divide a b) (b mod a =? 0).
Lemma BoolSpec_divide a b : BoolSpec (Z.divide a b) (~ Z.divide a b) ((b =? 0) || negb (a =? 0) && (b mod a =? 0))%bool.
Lemma divide_m1_l a : ( -1 | a ).
Lemma divide_pow_same_r a n (Hn : 1 <= n) : ( a | a^n ).
Definition coprime (a b:Z) : Prop := Z.gcd a b = 1.
Lemma BoolSpec_coprime a b : BoolSpec (Z.coprime a b) (~ Z.coprime a b) (Z.gcd a b =? 1).
Lemma Bezout_coprime_iff a b : Z.coprime a b <-> Z.Bezout a b 1.
Definition Bezout_coprime a b := proj1 (Bezout_coprime_iff a b).
Definition coprime_Bezout a b := proj2 (Bezout_coprime_iff a b).
#[global] Instance Symmetric_coprime : RelationClasses.Symmetric coprime.
Lemma coprime_0_l_iff z : coprime 0 z <-> Z.abs z = 1.
Lemma coprime_0_r_iff z : coprime z 0 <-> Z.abs z = 1.
Lemma coprime_1_l z : coprime 1 z.
Lemma coprime_1_r z : coprime z 1.
Lemma coprime_opp_l a b : coprime (- a) b <-> coprime a b.
Lemma coprime_opp_r a b : coprime a (- b) <-> coprime a b.
Lemma coprime_mod_l_iff a b : coprime (a mod b) b <-> coprime a b.
Lemma coprime_mod_r_iff a b : coprime a (b mod a) <-> coprime a b.
Lemma coprime_mul_r a b c : coprime a b -> coprime a c -> coprime a (b * c).
Lemma coprime_mul_l a b c : coprime a c -> coprime b c -> coprime (a * b) c.
Lemma coprime_pow_r a b n : 0 <= n -> coprime a b -> coprime a (b ^ n).
Lemma coprime_pow_l a b n : 0 <= n -> coprime a b -> coprime (a ^ n) b.
Definition prime p := 1 < p /\ forall n, 1 < n < p -> ~ (n|p).
Lemma not_prime_0 : not (prime 0).
Lemma not_prime_1 : not (prime 1).
Lemma prime_2 : prime 2.
Lemma prime_3 : prime 3.
Lemma prime_ge_2 p : prime p -> 2 <= p.
Lemma divide_prime_r a p (Hp : prime p) (Hd : (a | p)) :
a = -p \/ a = -1 \/ a = 1 \/ a = p.
Lemma divide_prime_r_iff a p (Hp : prime p) :
(a | p) <-> a = -p \/ a = -1 \/ a = 1 \/ a = p.
Lemma not_prime_square a : ~ prime (a * a).
Lemma coprime_prime_l p a (Hp : prime p) (Ha : ~ (p | a)) : coprime p a.
Lemma coprime_prime_l_iff p a (Hp : prime p) : coprime p a <-> ~ (p | a).
Lemma coprime_prime_small p a (Hp : prime p) (Ha : 1 <= a < p) : coprime p a.
Lemma divide_prime_mul a b p (Hp : prime p) :
(p | a * b) <-> (p | a) \/ (p | b).
Lemma divide_prime_prime p q (Hp : prime p) (Hq : prime q) :
( p | q ) -> p = q.
Lemma divide_prime_prime_iff p q (Hp : prime p) (Hq : prime q) :
( p | q ) <-> p = q.
Theorem divide_prime_pp p q n (Hp : prime p) (Hq : prime q) (Hn : 0 <= n) :
(p | q^n) -> p = q.
Theorem divide_prime_pp_iff p q n (Hp : prime p) (Hq : prime q) (Hn : 1 <= n) :
(p | q^n) <-> p = q.
Section extended_euclid_algorithm.
Variables a b : Z.
Local Lemma extgcd_rec_helper r1 r2 q :
Z.gcd r1 r2 = Z.gcd a b -> Z.gcd (r2 - q * r1) r1 = Z.gcd a b.
Let f := S(S(Z.to_nat(Z.log2_up(Z.log2_up(Z.abs(a*b)))))).
Local Definition extgcd_rec : forall r1 u1 v1 r2 u2 v2,
(True -> 0 <= r1 /\ 0 <= r2 /\ r1 = u1 * a + v1 * b /\ r2 = u2 * a + v2 * b /\
Z.gcd r1 r2 = Z.gcd a b)
-> { '(u, v, d) | True -> u * a + v * b = d /\ d = Z.gcd a b}.
Definition extgcd : Z*Z*Z.
Lemma extgcd_correct [u v d] : extgcd = (u, v, d) -> u * a + v * b = d /\ d = Z.gcd a b.
End extended_euclid_algorithm.
End Z.
Module Z.
Local Open Scope Z_scope.
Lemma mod0_divide : forall a b, (b | a) -> a mod b = 0.
Lemma absle_divide a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.
Lemma BoolSpec_divide_nz a b (H : a <> 0) : BoolSpec (Z.divide a b) (~ Z.divide a b) (b mod a =? 0).
Lemma BoolSpec_divide a b : BoolSpec (Z.divide a b) (~ Z.divide a b) ((b =? 0) || negb (a =? 0) && (b mod a =? 0))%bool.
Lemma divide_m1_l a : ( -1 | a ).
Lemma divide_pow_same_r a n (Hn : 1 <= n) : ( a | a^n ).
Definition coprime (a b:Z) : Prop := Z.gcd a b = 1.
Lemma BoolSpec_coprime a b : BoolSpec (Z.coprime a b) (~ Z.coprime a b) (Z.gcd a b =? 1).
Lemma Bezout_coprime_iff a b : Z.coprime a b <-> Z.Bezout a b 1.
Definition Bezout_coprime a b := proj1 (Bezout_coprime_iff a b).
Definition coprime_Bezout a b := proj2 (Bezout_coprime_iff a b).
#[global] Instance Symmetric_coprime : RelationClasses.Symmetric coprime.
Lemma coprime_0_l_iff z : coprime 0 z <-> Z.abs z = 1.
Lemma coprime_0_r_iff z : coprime z 0 <-> Z.abs z = 1.
Lemma coprime_1_l z : coprime 1 z.
Lemma coprime_1_r z : coprime z 1.
Lemma coprime_opp_l a b : coprime (- a) b <-> coprime a b.
Lemma coprime_opp_r a b : coprime a (- b) <-> coprime a b.
Lemma coprime_mod_l_iff a b : coprime (a mod b) b <-> coprime a b.
Lemma coprime_mod_r_iff a b : coprime a (b mod a) <-> coprime a b.
Lemma coprime_mul_r a b c : coprime a b -> coprime a c -> coprime a (b * c).
Lemma coprime_mul_l a b c : coprime a c -> coprime b c -> coprime (a * b) c.
Lemma coprime_pow_r a b n : 0 <= n -> coprime a b -> coprime a (b ^ n).
Lemma coprime_pow_l a b n : 0 <= n -> coprime a b -> coprime (a ^ n) b.
Definition prime p := 1 < p /\ forall n, 1 < n < p -> ~ (n|p).
Lemma not_prime_0 : not (prime 0).
Lemma not_prime_1 : not (prime 1).
Lemma prime_2 : prime 2.
Lemma prime_3 : prime 3.
Lemma prime_ge_2 p : prime p -> 2 <= p.
Lemma divide_prime_r a p (Hp : prime p) (Hd : (a | p)) :
a = -p \/ a = -1 \/ a = 1 \/ a = p.
Lemma divide_prime_r_iff a p (Hp : prime p) :
(a | p) <-> a = -p \/ a = -1 \/ a = 1 \/ a = p.
Lemma not_prime_square a : ~ prime (a * a).
Lemma coprime_prime_l p a (Hp : prime p) (Ha : ~ (p | a)) : coprime p a.
Lemma coprime_prime_l_iff p a (Hp : prime p) : coprime p a <-> ~ (p | a).
Lemma coprime_prime_small p a (Hp : prime p) (Ha : 1 <= a < p) : coprime p a.
Lemma divide_prime_mul a b p (Hp : prime p) :
(p | a * b) <-> (p | a) \/ (p | b).
Lemma divide_prime_prime p q (Hp : prime p) (Hq : prime q) :
( p | q ) -> p = q.
Lemma divide_prime_prime_iff p q (Hp : prime p) (Hq : prime q) :
( p | q ) <-> p = q.
Theorem divide_prime_pp p q n (Hp : prime p) (Hq : prime q) (Hn : 0 <= n) :
(p | q^n) -> p = q.
Theorem divide_prime_pp_iff p q n (Hp : prime p) (Hq : prime q) (Hn : 1 <= n) :
(p | q^n) <-> p = q.
Section extended_euclid_algorithm.
Variables a b : Z.
Local Lemma extgcd_rec_helper r1 r2 q :
Z.gcd r1 r2 = Z.gcd a b -> Z.gcd (r2 - q * r1) r1 = Z.gcd a b.
Let f := S(S(Z.to_nat(Z.log2_up(Z.log2_up(Z.abs(a*b)))))).
Local Definition extgcd_rec : forall r1 u1 v1 r2 u2 v2,
(True -> 0 <= r1 /\ 0 <= r2 /\ r1 = u1 * a + v1 * b /\ r2 = u2 * a + v2 * b /\
Z.gcd r1 r2 = Z.gcd a b)
-> { '(u, v, d) | True -> u * a + v * b = d /\ d = Z.gcd a b}.
Definition extgcd : Z*Z*Z.
Lemma extgcd_correct [u v d] : extgcd = (u, v, d) -> u * a + v * b = d /\ d = Z.gcd a b.
End extended_euclid_algorithm.
End Z.