Definition Zdivides (a b : Z) : Prop := exists q : Z, (q * a)%Z = b.



Section zdivides.

Lemma Zdivides_ref : forall a : Z, Zdivides a a.

Lemma Zdivides_trans :
 forall a b c : Z, Zdivides a b -> Zdivides b c -> Zdivides a c.

Lemma Zdivides_zero_rht : forall z : Z, Zdivides z 0.

Lemma Zdivides_zero_lft : forall z : Z, Zdivides 0 z -> z = 0%Z.

Lemma Zdivides_one : forall z : Z, Zdivides 1 z.


Lemma Zdivides_mult_intro_lft :
 forall a b c : Z, Zdivides (a * b) c -> Zdivides b c.

Lemma Zdivides_mult_intro_rht :
 forall a b c : Z, Zdivides (a * b) c -> Zdivides a c.

Lemma Zdivides_mult_lft : forall a b : Z, Zdivides b (a * b).

Lemma Zdivides_mult_rht : forall a b : Z, Zdivides a (a * b).

Lemma Zdivides_mult_elim_lft :
 forall a b c : Z, Zdivides a c -> Zdivides a (b * c).

Lemma Zdivides_mult_elim_rht :
 forall a b c : Z, Zdivides a b -> Zdivides a (b * c).

Lemma Zdivides_mult_cancel_lft :
 forall a b c : Z, Zdivides a b -> Zdivides (c * a) (c * b).

Lemma Zdivides_mult_cancel_rht :
 forall a b c : Z, Zdivides a b -> Zdivides (a * c) (b * c).

Let Zdiv_one_is_one : forall a : Z, (a > 0)%Z -> Zdivides a 1 -> a = 1%Z.
Defined.

Lemma Zdivides_antisymm :
 forall a b : Z,
 (a > 0)%Z -> (b > 0)%Z -> Zdivides a b -> Zdivides b a -> a = b.

Lemma Zdivides_plus_elim :
 forall a b c : Z, Zdivides a b -> Zdivides a c -> Zdivides a (b + c).

Lemma Zdivides_opp_elim_lft :
 forall a b : Z, Zdivides a b -> Zdivides (- a) b.

Lemma Zdivides_opp_elim_rht :
 forall a b : Z, Zdivides a b -> Zdivides a (- b).

Lemma Zdivides_opp_elim :
 forall a b : Z, Zdivides a b -> Zdivides (- a) (- b).

Lemma Zdivides_opp_intro_lft :
 forall a b : Z, Zdivides (- a) b -> Zdivides a b.

Lemma Zdivides_opp_intro_rht :
 forall a b : Z, Zdivides a (- b) -> Zdivides a b.

Lemma Zdivides_opp_intro :
 forall a b : Z, Zdivides (- a) (- b) -> Zdivides a b.

Lemma Zdivides_minus_elim :
 forall a b c : Z, Zdivides a b -> Zdivides a c -> Zdivides a (b - c).

Lemma Zdivides_mult_elim :
 forall a b c d : Z, Zdivides a b -> Zdivides c d -> Zdivides (a * c) (b * d).

Lemma Zdivides_mult_ll :
 forall a b c d : Z,
 (a * b)%Z = (c * d)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zdivides_mult_lr :
 forall a b c d : Z,
 (a * b)%Z = (d * c)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zdivides_mult_rl :
 forall a b c d : Z,
 (b * a)%Z = (c * d)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zdivides_mult_rr :
 forall a b c d : Z,
 (b * a)%Z = (d * c)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zdivides_abs_elim_lft :
 forall a b : Z, Zdivides a b -> Zdivides (Zabs a) b.

Lemma Zdivides_abs_elim_rht :
 forall a b : Z, Zdivides a b -> Zdivides a (Zabs b).

Lemma Zdivides_abs_elim :
 forall a b : Z, Zdivides a b -> Zdivides (Zabs a) (Zabs b).

Lemma Zdivides_abs_intro_lft :
 forall a b : Z, Zdivides (Zabs a) b -> Zdivides a b.

Lemma Zdivides_abs_intro_rht :
 forall a b : Z, Zdivides a (Zabs b) -> Zdivides a b.

Lemma Zdivides_abs_intro :
 forall a b : Z, Zdivides (Zabs a) (Zabs b) -> Zdivides a b.

Lemma Zdivisor_pos_le :
 forall a b : Z, (a > 0)%Z -> Zdivides b a -> (a >= b)%Z.

Lemma Zdivisor_small :
 forall a b : Z, Zdivides b a -> (Zabs a < b)%Z -> a = 0%Z.


Lemma Zmodeq_small :
 forall a b c : Z,
 (0 <= a < c)%Z -> (0 <= b < c)%Z -> Zdivides c (a - b) -> a = b.

Lemma Zdiv_remainder_unique :
 forall a b q1 r1 q2 r2 : Z,
 a = (q1 * b + r1)%Z ->
 (0 <= r1 < b)%Z -> a = (q2 * b + r2)%Z -> (0 <= r2 < b)%Z -> r1 = r2.

Lemma Zdiv_quotient_unique :
 forall a b q1 r1 q2 r2 : Z,
 a = (q1 * b + r1)%Z ->
 (0 <= r1 < b)%Z -> a = (q2 * b + r2)%Z -> (0 <= r2 < b)%Z -> q1 = q2.

Lemma Zmod0_Zopp :
 forall a b : Z, b <> 0%Z -> (a mod b)%Z = 0%Z -> (a mod - b)%Z = 0%Z.

Lemma Zdiv_Zopp :
 forall a b : Z, (a mod b)%Z = 0%Z -> (a / - b)%Z = (- (a / b))%Z.

Lemma Zmod0_Zdivides_pos :
 forall a b : Z, (b > 0)%Z -> Zdivides b a -> (a mod b)%Z = 0%Z.

Lemma Zdivides_Zmod0_pos :
 forall a b : Z, (b > 0)%Z -> (a mod b)%Z = 0%Z -> Zdivides b a.

Lemma Zmod0_Zdivides :
 forall a b : Z, b <> 0%Z -> Zdivides b a -> (a mod b)%Z = 0%Z.

Lemma Zdivides_Zmod0 :
 forall a b : Z, b <> 0%Z -> (a mod b)%Z = 0%Z -> Zdivides b a.

Lemma Zmod_mult_cancel_lft : forall a b : Z, ((a * b) mod a)%Z = 0%Z.

Lemma Zmod_mult_cancel_rht : forall a b : Z, ((a * b) mod b)%Z = 0%Z.

Lemma Zdiv_mult_cancel_lft : forall a b : Z, a <> 0%Z -> (a * b / a)%Z = b.

Lemma Zdiv_mult_cancel_rht : forall a b : Z, b <> 0%Z -> (a * b / b)%Z = a.

Lemma Zdiv_plus_elim :
 forall a b d : Z,
 Zdivides d a -> Zdivides d b -> ((a + b) / d)%Z = (a / d + b / d)%Z.

Lemma Zdiv_elim :
 forall a b d : Z,
 d <> 0%Z -> Zdivides d a -> Zdivides d b -> (a / d)%Z = (b / d)%Z -> a = b.

Lemma Zabs_div_lft : forall a : Z, (Zabs a / a)%Z = Zsgn a.


Lemma Zabs_div_rht : forall a : Z, (a / Zabs a)%Z = Zsgn a.

Lemma Zdiv_same : forall a : Z, a <> 0%Z -> (a / a)%Z = 1%Z.

Lemma Zmult_div_simpl_1 :
 forall a b c d : Z,
 (a * b)%Z = (c * d)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zmult_div_simpl_2 :
 forall a b c d : Z,
 (a * b)%Z = (d * c)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zmult_div_simpl_3 :
 forall a b c d : Z,
 (b * a)%Z = (c * d)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zmult_div_simpl_4 :
 forall a b c d : Z,
 (b * a)%Z = (d * c)%Z -> a <> 0%Z -> Zdivides a c -> Zdivides d b.

Lemma Zdivides_dec : forall a b : Z, {Zdivides a b} + {~ Zdivides a b}.

End zdivides.


Section ineq.

Lemma Zmod_POS_nonNEG :
 forall a b p : positive, (Zpos a mod Zpos b)%Z <> Zneg p.

Lemma Zdiv_POS :
 forall a b : positive, (Zpos b * (Zpos a / Zpos b) <= Zpos a)%Z.

Lemma Zmod_lt_POS :
 forall a b : positive, (Zpos a < Zpos b)%Z -> (Zpos a mod Zpos b)%Z = Zpos a.

Lemma Zdiv_lt_POS :
 forall a b : positive, (Zpos a < Zpos b)%Z -> (Zpos a / Zpos b)%Z = 0%Z.

End ineq.