(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   modulo
   Modulo Arithmetic.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import ZArith.

Require Import lemmas.
Require Import natZ.
Require Import exp.
Require Import divides.

(** (Mod a b n) means (a = b (mod n)) *)

Definition Mod (a b : Z) (n : nat) :=
  exists q : Z, a = (b + Z_of_nat n * q)%Z.

Lemma modpq_modp : forall (a b : Z) (p q : nat), Mod a b (p * q) -> Mod a b p.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   unfold Mod in |- *.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat p) q))) *)
   split with (Z_of_nat q * x)%Z.
(* Goal: @eq Z a (Z.add b (Z.mul (Z.of_nat p) (Z.mul (Z.of_nat q) x))) *)
   rewrite (Znat.inj_mult p q) in H0.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.mul x (Zneg xH)))) *)
   rewrite Zmult_assoc.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma mod_refl : forall (a : Z) (n : nat), Mod a a n.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   unfold Mod in |- *. intros.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add a (Z.mul n q))) *)
   split with 0%Z.
(* Goal: @eq Z b (Z.add b (Z.mul n Z0)) *)
   rewrite <- Zmult_0_r_reverse.
(* Goal: ZDivides n (Z.add (Z.mul n x) Z0) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite <- Zplus_0_r_reverse.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma mod_sym : forall (a b : Z) (n : nat), Mod a b n -> Mod b a n.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   unfold Mod in |- *. intros.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: ZMod (Z.opp a) (Z.opp b) n *)
   split with (- x)%Z.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: ZDivides n (Z.sub a b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite H0.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse.
(* Goal: @eq Z b (Z.add b (Z.add (Z.mul n x) (Z.mul n (Z.opp x)))) *)
   rewrite <- Zmult_plus_distr_r.
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add b (Z.opp b))) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_opp_r.
(* Goal: @eq Z b (Z.add b (Z.mul n Z0)) *)
   rewrite <- Zmult_0_r_reverse.
(* Goal: @eq Z b (Z.add b Z0) *)
   apply Zplus_0_r_reverse.
Qed.

Lemma mod_trans :
 forall (a b c : Z) (n : nat), Mod a b n -> Mod b c n -> Mod a c n.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   unfold Mod in |- *. intros.
(* Goal: False *)
   elim H. elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H2. rewrite H1.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.add a c) (Z.add (Z.add b d) (Z.mul n q))) *)
   split with (x + x0)%Z.
(* Goal: @eq Z (Z.add (Z.add c (Z.mul n x)) (Z.mul n x0)) (Z.add c (Z.mul n (Z.add x x0))) *)
   rewrite Zmult_plus_distr_r.
(* Goal: @eq Z (Z.add (Z.add c (Z.mul (Z.of_nat n) x)) (Z.mul (Z.of_nat n) x0)) (Z.add c (Z.add (Z.mul (Z.of_nat n) x) (Z.mul (Z.of_nat n) x0))) *)
   rewrite (Zplus_assoc c (Z_of_nat n * x) (Z_of_nat n * x0)).
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma eqmod : forall x y : Z, x = y -> forall n : nat, Mod x y n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H. apply mod_refl.
Qed.

Lemma mod_plus_compat :
 forall (a b c d : Z) (n : nat),
 Mod a b n -> Mod c d n -> Mod (a + c) (b + d) n.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   unfold Mod in |- *. intros.
(* Goal: False *)
   elim H. elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. split with (x + x0)%Z.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul a c) (Z.add (Z.mul b d) (Z.mul n q))) *)
   rewrite H1.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul a (Z.add d (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n q))) *)
   rewrite H2.
(* Goal: @eq Z (Z.add (Z.add b (Z.mul (Z.of_nat n) x0)) (Z.add d (Z.mul (Z.of_nat n) x))) (Z.add (Z.add b d) (Z.mul (Z.of_nat n) (Z.add x x0))) *)
   rewrite (Zplus_assoc (b + Z_of_nat n * x0) d (Z_of_nat n * x)).
(* Goal: @eq Z (Z.add (Z.add (Z.add b (Z.mul (Z.of_nat n) x0)) d) (Z.mul (Z.of_nat n) x)) (Z.add (Z.add b d) (Z.mul (Z.of_nat n) (Z.add x x0))) *)
   rewrite (Zplus_assoc_reverse b (Z_of_nat n * x0) d).
(* Goal: @eq Z (Z.add (Z.add b (Z.add (Z.mul (Z.of_nat n) x0) d)) (Z.mul (Z.of_nat n) x)) (Z.add (Z.add b d) (Z.mul (Z.of_nat n) (Z.add x x0))) *)
   rewrite (Zplus_comm (Z_of_nat n * x0) d).
(* Goal: @eq Z (Z.add (Z.add b (Z.add d (Z.mul n x0))) (Z.mul n x)) (Z.add (Z.add b d) (Z.mul n (Z.add x x0))) *)
   rewrite (Zplus_comm x x0).
(* Goal: @eq Z (Z.add (Z.add b (Z.add d (Z.mul (Z.of_nat n) x0))) (Z.mul (Z.of_nat n) x)) (Z.add (Z.add b d) (Z.mul (Z.of_nat n) (Z.add x0 x))) *)
   rewrite (Zmult_plus_distr_r (Z_of_nat n) x0 x).
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma mod_mult_compat :
 forall (a b c d : Z) (n : nat),
 Mod a b n -> Mod c d n -> Mod (a * c) (b * d) n.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   unfold Mod in |- *. intros.
(* Goal: False *)
   elim H. elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H1. rewrite H2. split with (x0 * d + x * b + Z_of_nat n * x0 * x)%Z.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul (Z.of_nat n) x0)) (Z.add d (Z.mul (Z.of_nat n) x))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_plus_distr_r (b + Z_of_nat n * x0) d (Z_of_nat n * x)).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.mul (Z.add b (Z.mul n x0)) (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite Zmult_plus_distr_l.
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.mul (Z.add b (Z.mul n x0)) (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite Zmult_plus_distr_l.
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul b (Z.mul (Z.of_nat n) x)) (Z.mul (Z.mul (Z.of_nat n) x0) (Z.mul (Z.of_nat n) x)))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_assoc b (Z_of_nat n) x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul (Z.mul b (Z.of_nat n)) x) (Z.mul (Z.mul (Z.of_nat n) x0) (Z.mul (Z.of_nat n) x)))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_comm b (Z_of_nat n)).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul (Z.mul (Z.of_nat n) b) x) (Z.mul (Z.mul (Z.of_nat n) x0) (Z.mul (Z.of_nat n) x)))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_assoc (Z_of_nat n * x0) (Z_of_nat n) x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul (Z.mul (Z.of_nat n) b) x) (Z.mul (Z.mul (Z.mul (Z.of_nat n) x0) (Z.of_nat n)) x))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_assoc_reverse (Z_of_nat n) x0 (Z_of_nat n)).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul (Z.mul (Z.of_nat n) b) x) (Z.mul (Z.mul (Z.of_nat n) (Z.mul x0 (Z.of_nat n))) x))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_assoc_reverse (Z_of_nat n) (x0 * Z_of_nat n) x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul (Z.mul (Z.of_nat n) b) x) (Z.mul (Z.of_nat n) (Z.mul (Z.mul x0 (Z.of_nat n)) x)))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_assoc_reverse (Z_of_nat n) b x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul (Z.of_nat n) x0) d)) (Z.add (Z.mul (Z.of_nat n) (Z.mul b x)) (Z.mul (Z.of_nat n) (Z.mul (Z.mul x0 (Z.of_nat n)) x)))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite <- (Zmult_plus_distr_r (Z_of_nat n) (b * x) (x0 * Z_of_nat n * x)).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.mul n (Z.add (Z.mul b x) (Z.mul (Z.mul x0 n) x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zplus_assoc_reverse (b * d)).
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.add (Z.mul (Z.mul (Z.of_nat n) x0) d) (Z.mul (Z.of_nat n) (Z.add (Z.mul b x) (Z.mul (Z.mul x0 (Z.of_nat n)) x))))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_assoc_reverse (Z_of_nat n) x0 d).
   rewrite <-
    (Zmult_plus_distr_r (Z_of_nat n) (x0 * d) (b * x + x0 * Z_of_nat n * x))
    .
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.mul x0 d) (Z.add (Z.mul b x) (Z.mul (Z.mul x0 (Z.of_nat n)) x))))) (Z.add (Z.mul b d) (Z.mul (Z.of_nat n) (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul (Z.of_nat n) x0) x)))) *)
   rewrite (Zmult_comm x0 (Z_of_nat n)).
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul b x)) (Z.mul (Z.mul n x0) x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_comm b x).
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma mod_sqr_compat :
 forall (a b : Z) (n : nat), Mod a b n -> Mod (a * a) (b * b) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. apply mod_mult_compat. assumption. assumption.
Qed.

Lemma mod_exp_compat :
 forall (a b : Z) (n : nat),
 Mod a b n -> forall m : nat, Mod (Exp a m) (Exp b m) n.
Proof.
(* Goal: forall m : nat, Mod (Exp a m) (Zpos xH) n *)
   simple induction m.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *. apply mod_refl.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   intros m1 IHm. simpl in |- *.
(* Goal: Mod (Z.mul a (Exp a m1)) (Z.mul (Zpos xH) (Zpos xH)) n *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Zpos xH)) (Zpos xH) *)
   apply mod_mult_compat.
(* Goal: ZMod x Z0 n *)
   assumption. assumption.
Qed.

Lemma moda0_exp_compat :
 forall (a : Z) (n : nat),
 n > 0 -> Mod a 0 n -> forall m : nat, m > 0 -> Mod (Exp a m) 0 n.
Proof.
(* Goal: forall (a : Z) (n : nat) (_ : gt n O) (_ : Mod a Z0 n) (m : nat) (_ : gt m O), Mod (Exp a m) Z0 n *)
   intros a n.
(* Goal: forall (_ : gt n O) (_ : Mod a Z0 n) (m : nat) (_ : gt m O), Mod (Exp a m) Z0 n *)
   case n.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: Mod (Exp a O) Z0 (S n0) *)
(* Goal: forall (n : nat) (_ : gt (S n) O), Mod (Exp a (S n)) Z0 (S n0) *)
   elim (lt_irrefl 0).
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: forall _ : gt m O, Mod (Exp a m) Z0 (S n0) *)
   case m.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: Mod (Exp a O) Z0 (S n0) *)
(* Goal: forall (n : nat) (_ : gt (S n) O), Mod (Exp a (S n)) Z0 (S n0) *)
   elim (lt_irrefl 0).
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: forall (n : nat) (_ : gt (S n) O), Mod (Exp a (S n)) Z0 (S n0) *)
   intro m0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: forall (x : Z) (_ : @eq Z a (Z.add b (Z.mul n x))), @ex Z (fun q : Z => @eq Z (Z.mul a c) (Z.add (Z.mul b d) (Z.mul n q))) *)
   elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul a (Z.add d (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n q))) *)
   rewrite H2.
(* Goal: Mod (Exp (Z.add Z0 (Z.mul (Z.of_nat (S n0)) x)) (S m0)) Z0 (S n0) *)
   split with (x * Exp (Z_of_nat (S n0) * x) m0)%Z.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.mul x (Zneg xH)))) *)
   rewrite Zmult_assoc.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma mod_opp_compat :
 forall (a b : Z) (n : nat), Mod a b n -> Mod (- a) (- b) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. elim H. intros.
(* Goal: ZMod (Z.opp a) (Z.opp b) n *)
   split with (- x)%Z. rewrite H0.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.opp x))) *)
   rewrite Zopp_eq_mult_neg_1.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.opp x))) *)
   rewrite Zopp_eq_mult_neg_1.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.opp x))) *)
   rewrite Zopp_eq_mult_neg_1.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.mul x (Zneg xH)))) *)
   rewrite Zmult_assoc.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul (Z.mul n x) (Zneg xH))) *)
   rewrite <- Zmult_plus_distr_l.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma mod_minus_compat :
 forall (a b c d : Z) (n : nat),
 Mod a b n -> Mod c d n -> Mod (a - c) (b - d) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: Mod (Z.add a (Z.opp c)) (Z.add b (Z.opp d)) n *)
   apply mod_plus_compat.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: Mod (Z.opp c) (Z.opp d) n *)
   apply mod_opp_compat.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma mod_nx_0_n : forall (n : nat) (x : Z), Mod (Z_of_nat n * x) 0 n.
Proof.
(* Goal: Mod (Z.mul (Z.of_nat n) x) Z0 n *)
   intros. unfold Mod in |- *.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   split with x.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *. reflexivity.
Qed.

Lemma moddivmin :
 forall (a b : Z) (n : nat), Mod a b n <-> Divides n (Zabs_nat (a - b)).
Proof.
(* Goal: forall (a b : Z) (n : nat), iff (Mod a b n) (Divides n (Z.abs_nat (Z.sub a b))) *)
   unfold Mod, Divides in |- *. split.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: ZDivides n (Z.sub a b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite H0.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse.
(* Goal: @eq Z a (Z.add (Z.add b a) (Z.opp b)) *)
   rewrite Zplus_comm.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse.
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add (Z.opp b) b)) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite (Zplus_comm (- b) b).
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add b (Z.opp b))) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_opp_r.
(* Goal: ZDivides n (Z.add (Z.mul n x) Z0) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite <- Zplus_0_r_reverse.
(* Goal: @ex nat (fun q : nat => @eq nat (Z.abs_nat (Z.mul (Z.of_nat n) x)) (Init.Nat.mul n q)) *)
(* Goal: forall _ : @ex nat (fun q : nat => @eq nat (Z.abs_nat (Z.sub a b)) (Init.Nat.mul n q)), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
   split with (Zabs_nat x).
(* Goal: @eq nat (Z.abs_nat (Z.mul (Z.of_nat n) x)) (Init.Nat.mul n (Z.abs_nat x)) *)
(* Goal: forall _ : @ex nat (fun q : nat => @eq nat (Z.abs_nat (Z.sub a b)) (Init.Nat.mul n q)), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
   pattern n at 2 in |- *.
(* Goal: lt (Z.abs_nat x) n *)
   rewrite <- (abs_inj n).
(* Goal: @eq nat (Z.abs_nat (Z.mul (Z.of_nat n) x)) (Init.Nat.mul (Z.abs_nat (Z.of_nat n)) (Z.abs_nat x)) *)
(* Goal: forall _ : @ex nat (fun q : nat => @eq nat (Z.abs_nat (Z.sub a b)) (Init.Nat.mul n q)), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
   apply abs_mult.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. elim H. intros.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
   elim (Zle_or_lt b a).
(* Goal: forall _ : Z.le b a, @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
(* Goal: forall _ : Z.lt a b, @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
   split with (Z_of_nat x).
(* Goal: @eq Z a (Z.add b (Z.opp (Z.mul (Z.of_nat x) (Z.of_nat n)))) *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z a (Z.add b (Z.mul n x)) *)
   rewrite <- H0.
(* Goal: Z.lt x (Z.of_nat (Z.abs_nat n)) *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   rewrite inj_abs_pos.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z a (Z.add (Z.add b a) (Z.opp b)) *)
   rewrite Zplus_comm.
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z a (Z.add (Z.add (Z.opp b) b) a) *)
   rewrite Zplus_opp_l.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *. reflexivity.
(* Goal: Z.ge n Z0 *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   apply Zle_ge.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   replace 0%Z with (b - b)%Z. unfold Zminus in |- *.
(* Goal: ZMod x Z0 n *)
   apply Zplus_le_compat_r. assumption.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: @eq Z (Z.add b (Z.opp b)) Z0 *)
   apply Zplus_opp_r.
(* Goal: forall _ : Z.lt a b, @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul (Z.of_nat n) q))) *)
   split with (- Z_of_nat x)%Z.
(* Goal: @eq Z a (Z.add b (Z.opp (Z.mul q n))) *)
(* Goal: Z.lt n Z0 *)
   rewrite Zmult_comm.
(* Goal: @eq Z a (Z.add b (Z.mul (Z.opp q) n)) *)
(* Goal: Z.lt n Z0 *)
   rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z a (Z.add b (Z.opp (Z.mul (Z.of_nat x) (Z.of_nat n)))) *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z a (Z.add b (Z.opp (Z.of_nat (Init.Nat.mul x n)))) *)
   rewrite mult_comm.
(* Goal: @eq Z a (Z.add b (Z.mul n x)) *)
   rewrite <- H0.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.add b (Z.mul n x)) (Z.add b (Z.mul (Z.of_nat (Z.abs_nat n)) q))) *)
   rewrite inj_abs_neg.
(* Goal: @eq Z (Z.add b (Z.mul n x)) (Z.add b (Z.mul n (Z.opp (Z.opp x)))) *)
(* Goal: Z.lt n Z0 *)
   rewrite Zopp_involutive.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: Z.lt (Z.add a (Z.opp b)) (Z.add b (Z.opp b)) *)
(* Goal: @eq Z (Z.sub b b) Z0 *)
   rewrite (Zplus_comm a).
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add b (Z.opp b))) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_opp_r.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *. reflexivity.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   replace 0%Z with (b - b)%Z. unfold Zminus in |- *.
(* Goal: Z.lt (Z.add a (Z.opp b)) (Z.add b (Z.opp b)) *)
(* Goal: @eq Z (Z.sub b b) Z0 *)
   rewrite (Zplus_comm a). rewrite (Zplus_comm b). apply Zplus_lt_compat_l.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *. apply Zplus_opp_r.
Qed.

Lemma moddec : forall (a b : Z) (n : nat), Mod a b n \/ ~ Mod a b n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   elim (moddivmin a b n). intros.
(* Goal: or (Mod a b n) (not (Mod a b n)) *)
   elim (divdec (Zabs_nat (a - b)) n).
(* Goal: ZMod x Z0 n *)
   left. apply H0. assumption.
(* Goal: ZMod x Z0 n *)
   right. intro. elim H1. apply H. assumption.
Qed.

Lemma mod_0not1 : forall n : nat, n > 1 -> ~ Mod 0 1 n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: False *)
   absurd (Divides n 1).
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: False *)
(* Goal: Divides n (S O) *)
   elim (le_not_lt n 1).
(* Goal: le n (S O) *)
(* Goal: lt (S O) n *)
(* Goal: Divides n (S O) *)
   apply div_le1.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: Divides n (S O) *)
   elim (moddivmin 0 1 n).
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: Divides n (S O) *)
   apply H1.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma mod_exp1 :
 forall (a : Z) (n : nat), Mod a 1 n -> forall m : nat, Mod (Exp a m) 1 n.
Proof.
(* Goal: forall (a : Z) (n : nat) (_ : Mod a (Zpos xH) n) (m : nat), Mod (Exp a m) (Zpos xH) n *)
   intros a n H.
(* Goal: forall m : nat, Mod (Exp a m) (Zpos xH) n *)
   simple induction m.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: Mod (Zpos xH) (Zpos xH) n *)
(* Goal: forall (n0 : nat) (_ : Mod (Exp a n0) (Zpos xH) n), Mod (Exp a (S n0)) (Zpos xH) n *)
   apply mod_refl.
(* Goal: forall (n0 : nat) (_ : Mod (Exp a n0) (Zpos xH) n), Mod (Exp a (S n0)) (Zpos xH) n *)
   intros m1 IH.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: Mod (Z.mul a (Exp a m1)) (Zpos xH) n *)
   replace 1%Z with (1 * 1)%Z.
(* Goal: Mod (Z.mul a (Exp a m1)) (Z.mul (Zpos xH) (Zpos xH)) n *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Zpos xH)) (Zpos xH) *)
   apply mod_mult_compat.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: Mod (Exp a m1) (Zpos xH) n *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Zpos xH)) (Zpos xH) *)
   apply IH.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma mod_repr_non_0 :
 forall (n : nat) (x : Z), (0 < x < Z_of_nat n)%Z -> ~ Mod x 0 n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim (moddivmin x 0 n).
(* Goal: forall (_ : forall _ : Mod x Z0 n, Divides n (Z.abs_nat (Z.sub x Z0))) (_ : forall _ : Divides n (Z.abs_nat (Z.sub x Z0)), Mod x Z0 n), False *)
   rewrite <- Zminus_0_l_reverse.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim (le_not_lt n (Zabs_nat x)).
(* Goal: le n (Z.abs_nat x) *)
(* Goal: lt (Z.abs_nat x) n *)
   apply div_le.
(* Goal: lt O (Z.abs_nat x) *)
(* Goal: Divides n (Z.abs_nat x) *)
(* Goal: lt (Z.abs_nat x) n *)
   change (Zabs_nat 0 < Zabs_nat x) in |- *.
(* Goal: lt (Z.abs_nat x) (Z.abs_nat (Z.of_nat n)) *)
   apply ltzlt.
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   unfold Zle in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: not (@eq comparison Lt Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   discriminate.
(* Goal: Z.le x n *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   apply Zlt_le_weak.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: Divides n (Z.abs_nat x) *)
(* Goal: lt (Z.abs_nat x) n *)
   apply H3.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: lt (Z.abs_nat x) n *)
   rewrite <- (abs_inj n).
(* Goal: lt (Z.abs_nat x) (Z.abs_nat (Z.of_nat n)) *)
   apply ltzlt.
(* Goal: Z.le x n *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   apply Zlt_le_weak.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: Z.le Z0 (Z.of_nat n) *)
(* Goal: Z.lt x (Z.of_nat n) *)
   change (Z_of_nat 0 <= Z_of_nat n)%Z in |- *.
(* Goal: Z.le (Z.of_nat O) (Z.of_nat n) *)
(* Goal: Z.lt x (Z.of_nat n) *)
   apply Znat.inj_le.
(* Goal: le O n *)
(* Goal: Z.lt x (Z.of_nat n) *)
   apply le_O_n.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma mod_repr_eq :
 forall (p : nat) (x y : Z),
 0 < p ->
 (0 < x < Z_of_nat p)%Z -> (0 < y < Z_of_nat p)%Z -> Mod x y p -> x = y.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. unfold Mod in H2.
(* Goal: @eq Z x y *)
   elim H2. intros q Hq.
(* Goal: @eq Z x y *)
   rewrite Hq in H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   elim H0. elim H1. intros.
(* Goal: @eq Z x y *)
   elim (Zle_or_lt 0 q).
(* Goal: not (ZMod x Z0 n) *)
   intro. elim (Zle_lt_or_eq 0 q).

   (* 0<q *)
(* Goal: not (ZMod x Z0 n) *)
   intro. elim (Zlt_not_le 0 y).
(* Goal: ZMod x Z0 n *)
   assumption. apply Zplus_le_reg_l with (Z_of_nat p).
(* Goal: Z.le (Z.add (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) (Z.of_nat p)) (Z.add (Z.of_nat p) Z0) *)
   rewrite (Zplus_comm (Z_of_nat p)).
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   rewrite (Zplus_comm (Z_of_nat p)). simpl in |- *.
(* Goal: Z.le x n *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   apply Zlt_le_weak.
(* Goal: Z.lt (Z.add y (Z.of_nat p)) (Z.of_nat p) *)
(* Goal: forall _ : @eq Z Z0 q, @eq Z x y *)
(* Goal: Z.le Z0 q *)
(* Goal: forall _ : Z.lt q Z0, @eq Z x y *)
   apply Zle_lt_trans with (y + Z_of_nat p * q)%Z.
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) q)) (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) *)
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) Z0 *)
   apply Zplus_le_compat_l. pattern (Z_of_nat p) at 1 in |- *. 
(* Goal: (fun z : Z => Z.le z (Z.mul (Z.of_nat p) q)) (Z.of_nat p) *)
(* Goal: Z.lt (Z.add y (Z.mul (Z.of_nat p) q)) (Z.of_nat p) *)
(* Goal: forall _ : @eq Z Z0 q, @eq Z x y *)
(* Goal: Z.le Z0 q *)
(* Goal: forall _ : Z.lt q Z0, @eq Z x y *)
   rewrite <- Zmult_1_l with (Z_of_nat p).
(* Goal: Z.le (Z.mul (Zpos xH) (Z.of_nat p)) (Z.mul (Z.of_nat p) q) *)
(* Goal: Z.lt (Z.add y (Z.mul (Z.of_nat p) q)) (Z.of_nat p) *)
(* Goal: forall _ : @eq Z Z0 q, @eq Z x y *)
(* Goal: Z.le Z0 q *)
(* Goal: forall _ : Z.lt q Z0, @eq Z x y *)
   rewrite (Zmult_comm 1). apply Zle_mult_l.
(* Goal: Z.lt Z0 (Z.of_nat p) *)
(* Goal: Z.le q (Zneg xH) *)
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) Z0 *)
   change (Z_of_nat 0 < Z_of_nat p)%Z in |- *.
(* Goal: ZMod x Z0 n *)
   apply Znat.inj_lt. assumption.
(* Goal: ZMod x Z0 n *)
   change (Zsucc 0 <= q)%Z in |- *. apply Zlt_le_succ. assumption.
(* Goal: ZMod x Z0 n *)
   assumption.

   (* 0=q *)
(* Goal: not (ZMod x Z0 n) *)
   intro. rewrite <- H8 in Hq. rewrite Zmult_comm in Hq.
(* Goal: ZMod x Z0 n *)
   rewrite Zplus_comm in Hq. simpl in Hq. assumption.

(* Goal: ZMod x Z0 n *)
   assumption.

   (* q<0 *)
(* Goal: not (ZMod x Z0 n) *)
   intro. elim (Zlt_not_le 0 (y + Z_of_nat p * q)).
(* Goal: ZMod x Z0 n *)
   assumption. apply Zle_trans with (y + Z_of_nat p * -1)%Z.
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) q)) (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) *)
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) Z0 *)
   apply Zplus_le_compat_l. apply Zle_mult_l.
(* Goal: Z.lt Z0 (Z.of_nat p) *)
(* Goal: Z.le q (Zneg xH) *)
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) Z0 *)
   change (Z_of_nat 0 < Z_of_nat p)%Z in |- *. apply Znat.inj_lt.
(* Goal: ZMod x Z0 n *)
   assumption. apply Zlt_succ_le. simpl in |- *. assumption.
(* Goal: Z.le (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) Z0 *)
   apply Zplus_le_reg_l with (Z_of_nat p).
(* Goal: Z.le (Z.add (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) (Z.of_nat p)) (Z.add (Z.of_nat p) Z0) *)
   rewrite (Zplus_comm (Z_of_nat p)).
(* Goal: Z.le (Z.add (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) (Z.of_nat p)) (Z.add (Z.of_nat p) Z0) *)
   rewrite (Zplus_comm (Z_of_nat p)).
(* Goal: Z.le (Z.add (Z.add y (Z.mul (Z.of_nat p) (Zneg xH))) (Z.of_nat p)) (Z.add Z0 (Z.of_nat p)) *)
   rewrite (Zmult_comm (Z_of_nat p)).
(* Goal: Z.le (Z.add (Z.add y (Z.mul (Zneg xH) (Z.of_nat p))) (Z.of_nat p)) (Z.add Z0 (Z.of_nat p)) *)
   rewrite (Zopp_mult_distr_l_reverse 1). rewrite Zmult_1_l.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse. rewrite Zplus_opp_l.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   rewrite (Zplus_comm y 0). simpl in |- *. apply Zlt_le_weak.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

(** ZMod, same as Mod but only uses Z. *)

Definition ZMod (a b n : Z) := exists q : Z, a = (b + n * q)%Z.

Lemma zmodpq_modp : forall a b p q : Z, ZMod a b (p * q) -> ZMod a b p.
Proof.
(* Goal: ZMod (Z.mul n x) Z0 n *)
   unfold ZMod in |- *.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul p q))) *)
   split with (q * x)%Z.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.mul x (Zneg xH)))) *)
   rewrite Zmult_assoc.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma zmod_refl : forall a n : Z, ZMod a a n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   unfold ZMod in |- *. intros.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add a (Z.mul n q))) *)
   split with 0%Z.
(* Goal: @eq Z b (Z.add b (Z.mul n Z0)) *)
   rewrite <- Zmult_0_r_reverse.
(* Goal: ZDivides n (Z.add (Z.mul n x) Z0) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite <- Zplus_0_r_reverse.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma zmod_sym : forall a b n : Z, ZMod a b n -> ZMod b a n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   unfold ZMod in |- *. intros.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: ZMod (Z.opp a) (Z.opp b) n *)
   split with (- x)%Z.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: ZDivides n (Z.sub a b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite H0.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse.
(* Goal: @eq Z b (Z.add b (Z.add (Z.mul n x) (Z.mul n (Z.opp x)))) *)
   rewrite <- Zmult_plus_distr_r.
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add b (Z.opp b))) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_opp_r.
(* Goal: @eq Z b (Z.add b (Z.mul n Z0)) *)
   rewrite <- Zmult_0_r_reverse.
(* Goal: @eq Z b (Z.add b Z0) *)
   apply Zplus_0_r_reverse.
Qed.

Lemma zmod_trans : forall a b c n : Z, ZMod a b n -> ZMod b c n -> ZMod a c n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   unfold ZMod in |- *. intros.
(* Goal: False *)
   elim H. elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H2. rewrite H1.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.add a c) (Z.add (Z.add b d) (Z.mul n q))) *)
   split with (x + x0)%Z.
(* Goal: @eq Z (Z.add (Z.add c (Z.mul n x)) (Z.mul n x0)) (Z.add c (Z.mul n (Z.add x x0))) *)
   rewrite Zmult_plus_distr_r.
(* Goal: @eq Z (Z.add (Z.add c (Z.mul n x)) (Z.mul n x0)) (Z.add c (Z.add (Z.mul n x) (Z.mul n x0))) *)
   rewrite (Zplus_assoc c (n * x) (n * x0)).
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma zeqmod : forall x y : Z, x = y -> forall n : Z, ZMod x y n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H. apply zmod_refl.
Qed.

Lemma zmod_plus_compat :
 forall a b c d n : Z, ZMod a b n -> ZMod c d n -> ZMod (a + c) (b + d) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   unfold ZMod in |- *. intros.
(* Goal: False *)
   elim H. elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. split with (x + x0)%Z.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul a c) (Z.add (Z.mul b d) (Z.mul n q))) *)
   rewrite H1.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul a (Z.add d (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n q))) *)
   rewrite H2.
(* Goal: @eq Z (Z.add (Z.add b (Z.mul n x0)) (Z.add d (Z.mul n x))) (Z.add (Z.add b d) (Z.mul n (Z.add x x0))) *)
   rewrite (Zplus_assoc (b + n * x0) d (n * x)).
(* Goal: @eq Z (Z.add (Z.add (Z.add b (Z.mul n x0)) d) (Z.mul n x)) (Z.add (Z.add b d) (Z.mul n (Z.add x x0))) *)
   rewrite (Zplus_assoc_reverse b (n * x0) d).
(* Goal: @eq Z (Z.add (Z.add b (Z.add (Z.mul n x0) d)) (Z.mul n x)) (Z.add (Z.add b d) (Z.mul n (Z.add x x0))) *)
   rewrite (Zplus_comm (n * x0) d).
(* Goal: @eq Z (Z.add (Z.add b (Z.add d (Z.mul n x0))) (Z.mul n x)) (Z.add (Z.add b d) (Z.mul n (Z.add x x0))) *)
   rewrite (Zplus_comm x x0).
(* Goal: @eq Z (Z.add (Z.add b (Z.add d (Z.mul n x0))) (Z.mul n x)) (Z.add (Z.add b d) (Z.mul n (Z.add x0 x))) *)
   rewrite (Zmult_plus_distr_r n x0 x).
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma zmod_mult_compat :
 forall a b c d n : Z, ZMod a b n -> ZMod c d n -> ZMod (a * c) (b * d) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   unfold ZMod in |- *. intros.
(* Goal: False *)
   elim H. elim H0.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H1. rewrite H2. split with (x0 * d + x * b + n * x0 * x)%Z.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x0)) (Z.add d (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_plus_distr_r (b + n * x0) d (n * x)).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.mul (Z.add b (Z.mul n x0)) (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite Zmult_plus_distr_l.
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.mul (Z.add b (Z.mul n x0)) (Z.mul n x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite Zmult_plus_distr_l.
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul b (Z.mul n x)) (Z.mul (Z.mul n x0) (Z.mul n x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_assoc b n x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul (Z.mul b n) x) (Z.mul (Z.mul n x0) (Z.mul n x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_comm b n).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul (Z.mul n b) x) (Z.mul (Z.mul n x0) (Z.mul n x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_assoc (n * x0) n x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul (Z.mul n b) x) (Z.mul (Z.mul (Z.mul n x0) n) x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_assoc_reverse n x0 n).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul (Z.mul n b) x) (Z.mul (Z.mul n (Z.mul x0 n)) x))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_assoc_reverse n (x0 * n) x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul (Z.mul n b) x) (Z.mul n (Z.mul (Z.mul x0 n) x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_assoc_reverse n b x).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.add (Z.mul n (Z.mul b x)) (Z.mul n (Z.mul (Z.mul x0 n) x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite <- (Zmult_plus_distr_r n (b * x) (x0 * n * x)).
(* Goal: @eq Z (Z.add (Z.add (Z.mul b d) (Z.mul (Z.mul n x0) d)) (Z.mul n (Z.add (Z.mul b x) (Z.mul (Z.mul x0 n) x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zplus_assoc_reverse (b * d)).
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.add (Z.mul (Z.mul n x0) d) (Z.mul n (Z.add (Z.mul b x) (Z.mul (Z.mul x0 n) x))))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_assoc_reverse n x0 d).
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.add (Z.mul n (Z.mul x0 d)) (Z.mul n (Z.add (Z.mul b x) (Z.mul (Z.mul x0 n) x))))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite <- (Zmult_plus_distr_r n (x0 * d) (b * x + x0 * n * x)).
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.mul x0 d) (Z.add (Z.mul b x) (Z.mul (Z.mul x0 n) x))))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_comm x0 n).
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul b x)) (Z.mul (Z.mul n x0) x)))) (Z.add (Z.mul b d) (Z.mul n (Z.add (Z.add (Z.mul x0 d) (Z.mul x b)) (Z.mul (Z.mul n x0) x)))) *)
   rewrite (Zmult_comm b x).
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma zmod_sqr_compat :
 forall a b n : Z, ZMod a b n -> ZMod (a * a) (b * b) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. apply zmod_mult_compat. assumption. assumption.
Qed.

Lemma zmodmod : forall a b n : Z, ZMod a b n -> Mod a b (Zabs_nat n).
Proof.
(* Goal: forall (a b n : Z) (_ : ZMod a b n), Mod a b (Z.abs_nat n) *)
   unfold ZMod, Mod in |- *.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. elim H. intros.
(* Goal: ZDivides n (Z.sub a b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite H0.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.add b (Z.mul n x)) (Z.add b (Z.mul (Z.of_nat (Z.abs_nat n)) q))) *)
   elim (Zle_or_lt 0 n).
(* Goal: not (ZMod x Z0 n) *)
   intro. rewrite inj_abs_pos.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   split with x. reflexivity.
(* Goal: ZMod x Z0 n *)
   apply Zle_ge. assumption.
(* Goal: not (ZMod x Z0 n) *)
   intro. rewrite inj_abs_neg.
(* Goal: ZMod (Z.opp a) (Z.opp b) n *)
   split with (- x)%Z. rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.add b (Z.mul n x)) (Z.add b (Z.mul n (Z.opp (Z.opp x)))) *)
(* Goal: Z.lt n Z0 *)
   rewrite Zopp_mult_distr_r. rewrite Zopp_involutive.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma modzmod :
 forall (a b : Z) (n : nat), Mod a b n -> ZMod a b (Z_of_nat n).
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   unfold Mod, ZMod in |- *. intros. elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite H0. split with x.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma absmodzmod : forall a b n : Z, Mod a b (Zabs_nat n) -> ZMod a b n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim H. intros q Hq. 
(* Goal: ZMod a b n *)
   elim Zle_or_lt with 0%Z n.
(* Goal: not (ZMod x Z0 n) *)
   intro. split with q. rewrite inj_abs_pos in Hq.
(* Goal: ZMod x Z0 n *)
   assumption. apply Zle_ge. assumption.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. split with (- q)%Z. rewrite inj_abs_neg in Hq.
(* Goal: @eq Z a (Z.add b (Z.opp (Z.mul q n))) *)
(* Goal: Z.lt n Z0 *)
   rewrite Zmult_comm. rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z a (Z.add b (Z.opp (Z.mul q n))) *)
(* Goal: Z.lt n Z0 *)
   rewrite Zopp_mult_distr_l_reverse in Hq. rewrite Zmult_comm.
(* Goal: ZMod x Z0 n *)
   assumption. assumption.
Qed.

Lemma zmod_exp_compat :
 forall a b n : Z, ZMod a b n -> forall m : Z, ZMod (ZExp a m) (ZExp b m) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: ZMod (ZExp a m) (ZExp b m) n *)
   apply absmodzmod.
(* Goal: Mod (ZExp a m) Z0 (Z.abs_nat n) *)
(* Goal: Z.ge n Z0 *)
   rewrite expzexp.
(* Goal: Mod (ZExp a m) Z0 (Z.abs_nat n) *)
(* Goal: Z.ge n Z0 *)
   rewrite expzexp.
(* Goal: Mod (Exp a (Z.abs_nat m)) (Exp b (Z.abs_nat m)) (Z.abs_nat n) *)
   apply mod_exp_compat.
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   apply zmodmod.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma zmoda0_exp_compat :
 forall a n : Z,
 (n > 0)%Z -> ZMod a 0 n -> forall m : Z, (m > 0)%Z -> ZMod (ZExp a m) 0 n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. rewrite <- (inj_abs_pos n).
(* Goal: Mod (ZExp a m) Z0 (Z.abs_nat n) *)
(* Goal: Z.ge n Z0 *)
   apply modzmod. rewrite expzexp.
(* Goal: Mod (Exp a (Z.abs_nat m)) Z0 (Z.abs_nat n) *)
(* Goal: Z.ge n Z0 *)
   apply moda0_exp_compat.
(* Goal: gt (Z.abs_nat n) O *)
(* Goal: Mod a Z0 (Z.abs_nat n) *)
(* Goal: gt (Z.abs_nat m) O *)
(* Goal: Z.ge n Z0 *)
   change (Zabs_nat n > Zabs_nat 0) in |- *. apply gtzgt.
(* Goal: ZMod x Z0 n *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   apply Zeq_le. reflexivity.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: ZMod x Z0 n *)
   apply zmodmod. assumption.
(* Goal: gt (Z.abs_nat n) (Z.abs_nat (Zpos xH)) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   change (Zabs_nat m > Zabs_nat 0) in |- *. apply gtzgt.
(* Goal: ZMod x Z0 n *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   apply Zeq_le. reflexivity.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: ZMod x Z0 n *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
Qed.

Lemma zmod_opp_compat : forall a b n : Z, ZMod a b n -> ZMod (- a) (- b) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. elim H. intros.
(* Goal: ZMod (Z.opp a) (Z.opp b) n *)
   split with (- x)%Z. rewrite H0.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.opp x))) *)
   rewrite Zopp_eq_mult_neg_1.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.opp x))) *)
   rewrite Zopp_eq_mult_neg_1.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.opp x))) *)
   rewrite Zopp_eq_mult_neg_1.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul n (Z.mul x (Zneg xH)))) *)
   rewrite Zmult_assoc.
(* Goal: @eq Z (Z.mul (Z.add b (Z.mul n x)) (Zneg xH)) (Z.add (Z.mul b (Zneg xH)) (Z.mul (Z.mul n x) (Zneg xH))) *)
   rewrite <- Zmult_plus_distr_l.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.
Qed.

Lemma zmod_minus_compat :
 forall a b c d n : Z, ZMod a b n -> ZMod c d n -> ZMod (a - c) (b - d) n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: ZMod (Z.add a (Z.opp c)) (Z.add b (Z.opp d)) n *)
   apply zmod_plus_compat.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: ZMod (Z.opp c) (Z.opp d) n *)
   apply zmod_opp_compat.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma zmod_nx_0_n : forall n x : Z, ZMod (n * x) 0 n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. unfold ZMod in |- *.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   split with x.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *. reflexivity.
Qed.

Lemma zmoddivmin : forall a b n : Z, ZMod a b n <-> ZDivides n (a - b).
Proof.
(* Goal: and (Z.lt Z0 x) (Z.lt x (Z.of_nat (Z.abs_nat n))) *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   unfold ZMod, Divides in |- *. split.

   (* -> *)
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. elim H. intros.
(* Goal: ZDivides n (Z.sub a b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite H0.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse.
(* Goal: @eq Z a (Z.add (Z.add b a) (Z.opp b)) *)
   rewrite Zplus_comm.
(* Goal: ZDivides n (Z.add (Z.add (Z.mul n x) (Z.opp b)) b) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_assoc_reverse.
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add (Z.opp b) b)) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite (Zplus_comm (- b) b).
(* Goal: ZDivides n (Z.add (Z.mul n x) (Z.add b (Z.opp b))) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite Zplus_opp_r.
(* Goal: ZDivides n (Z.add (Z.mul n x) Z0) *)
(* Goal: forall _ : ZDivides n (Z.sub a b), @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   rewrite <- Zplus_0_r_reverse.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   split with x.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   reflexivity.

   (* <- *)
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. elim H. intros.
(* Goal: @ex Z (fun q : Z => @eq Z a (Z.add b (Z.mul n q))) *)
   split with x.
(* Goal: @eq Z a (Z.add b (Z.mul n x)) *)
   rewrite <- H0.
(* Goal: @eq Z a (Z.add b (Z.sub a b)) *)
   unfold Zminus in |- *.
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z a (Z.add (Z.add b a) (Z.opp b)) *)
   rewrite Zplus_comm.
(* Goal: @eq Z a (Z.add (Z.opp b) (Z.add b a)) *)
   rewrite Zplus_assoc.
(* Goal: @eq Z a (Z.add (Z.add (Z.opp b) b) a) *)
   rewrite Zplus_opp_l.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   simpl in |- *. reflexivity.
Qed.

Lemma zmoddec : forall a b n : Z, ZMod a b n \/ ~ ZMod a b n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: or (ZMod a b n) (not (ZMod a b n)) *)
   elim (zmoddivmin a b n).
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: or (ZMod a b n) (not (ZMod a b n)) *)
   elim (zdivdec (a - b) n).
(* Goal: forall _ : ZDivides n (Z.sub a b), or (ZMod a b n) (not (ZMod a b n)) *)
(* Goal: forall _ : not (ZDivides n (Z.sub a b)), or (ZMod a b n) (not (ZMod a b n)) *)
   left.
(* Goal: ZMod a b n *)
(* Goal: forall _ : not (ZDivides n (Z.sub a b)), or (ZMod a b n) (not (ZMod a b n)) *)
   apply H0.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: forall _ : not (ZDivides n (Z.sub a b)), or (ZMod a b n) (not (ZMod a b n)) *)
   right.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: False *)
   elim H1.
(* Goal: ZDivides n (Z.sub a b) *)
   apply H.
(* Goal: ZMod x Z0 n *)
   assumption.
Qed.

Lemma zmod_0not1 : forall n : Z, (n > 1)%Z -> ~ ZMod 0 1 n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros. intro.
(* Goal: False *)
   elim (mod_0not1 (Zabs_nat n)).
(* Goal: gt (Z.abs_nat n) (Z.abs_nat (Zpos xH)) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   change (Zabs_nat n > Zabs_nat 1) in |- *. apply gtzgt.
(* Goal: Z.le x n *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   apply Zlt_le_weak. apply Zlt_trans with 1%Z.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   unfold Zlt in |- *. simpl in |- *. reflexivity.
(* Goal: ZMod x Z0 n *)
   apply Zgt_lt. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.gt n (Zpos xH) *)
(* Goal: Mod Z0 (Zpos xH) (Z.abs_nat n) *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: ZMod x Z0 n *)
   assumption.
(* Goal: ZMod x Z0 n *)
   apply zmodmod. assumption.
Qed.

Lemma zmod_repr_non_0 : forall n x : Z, (0 < x < n)%Z -> ~ ZMod x 0 n.
Proof.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: not (ZMod x Z0 n) *)
   intro.
(* Goal: False *)
   elim H.
(* Goal: forall (_ : Z.lt Z0 x) (_ : Z.lt x n), False *)
   intros.
(* Goal: False *)
   elim (mod_repr_non_0 (Zabs_nat n) x).
(* Goal: and (Z.lt Z0 x) (Z.lt x (Z.of_nat (Z.abs_nat n))) *)
(* Goal: Mod x Z0 (Z.abs_nat n) *)
   split.
(* Goal: ZMod x Z0 n *)
   assumption. rewrite inj_abs_pos.
(* Goal: ZMod x Z0 n *)
   assumption. apply Zle_ge. apply Zle_trans with x.
(* Goal: ZMod x Z0 n *)
   apply Zlt_le_weak. assumption.
(* Goal: ZMod x Z0 n *)
   apply Zlt_le_weak. assumption.
(* Goal: ZMod x Z0 n *)
   apply zmodmod. assumption.
Qed.
