(* 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                                                     *)


(**
   divides.
   The division predicate.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import ZArith.
Require Import Wf_nat.

Require Import lemmas.
Require Import natZ.
Require Import dec.
Require Import exp.

(** * Division on nat *)

Definition Divides (n m : nat) : Prop := exists q : nat, m = n * q.

Lemma div_refl : forall a : nat, Divides a a.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. split with 1.
(* Goal: @eq nat a (Init.Nat.mul a (S O)) *)
   rewrite <- mult_n_Sm.
(* Goal: @eq nat a (Init.Nat.add (Init.Nat.mul a O) a) *)
   rewrite <- mult_n_O.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *. reflexivity.
Qed.

Lemma div_trans :
 forall p q r : nat, Divides p q -> Divides q r -> Divides p r.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: ZDivides a (Z.add b c) *)
   elim H0.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: Divides a (Init.Nat.mul b c) *)
   unfold Divides in |- *.
(* Goal: @ex nat (fun q : nat => @eq nat r (Init.Nat.mul p q)) *)
   split with (x0 * x).
(* Goal: @eq Z (Z.add b c) (Z.mul a (Z.add x y)) *)
   rewrite H1.
(* Goal: @eq Z (Z.add (Z.mul a x) c) (Z.mul a (Z.add x y)) *)
   rewrite H2.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a x) c) (Init.Nat.mul a (Init.Nat.mul x c)) *)
   rewrite mult_assoc.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
Qed.

Lemma div_antisym : forall a b : nat, Divides a b -> Divides b a -> a = b.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. elim H. elim H0. intros x Ha y Hb.
(* Goal: @eq nat a b *)
   rewrite Hb in Ha.
(* Goal: @eq nat a b *)
   rewrite mult_assoc_reverse in Ha.
(* Goal: @eq nat a b *)
   elim (mult_ppq_p0q1 a (y * x)). intro.
(* Goal: @eq nat a b *)
(* Goal: forall _ : @eq nat (Init.Nat.mul y x) (S O), @eq nat a b *)
(* Goal: @eq nat a (Init.Nat.mul a (Init.Nat.mul y x)) *)
   rewrite H1 in Hb.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in Hb. rewrite H1. rewrite Hb. reflexivity.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. elim (mult_pq1_p1q1 y x H1).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @eq nat a b *)
(* Goal: @eq nat a (Init.Nat.mul a (Init.Nat.mul y x)) *)
   rewrite H2 in Hb. rewrite <- mult_n_Sm in Hb. rewrite <- mult_n_O in Hb.
(* Goal: @eq nat a b *)
(* Goal: @eq nat a (Init.Nat.mul a (Init.Nat.mul y x)) *)
   simpl in Hb. symmetry  in |- *. assumption. assumption.
Qed.

Lemma div_le1 : forall n d : nat, Divides d (S n) -> d <= S n.
Proof.
(* Goal: Divides a (Init.Nat.mul b c) *)
   unfold Divides in |- *.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (x : nat) (_ : @eq nat (S n0) (Init.Nat.mul d x)), @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul d q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   intro q.
(* Goal: forall _ : @eq nat (S n) (Init.Nat.mul d q), le d (S n) *)
   case q.
(* Goal: @eq nat O (Init.Nat.mul d O) *)
(* Goal: forall (_ : @ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))) (_ : @ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   rewrite <- (mult_n_O d).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) O)) *)
(* Goal: forall (n : nat) (_ : @eq nat (S n0) (Init.Nat.mul (S n) q)), @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul (S n) q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   discriminate H0.
(* Goal: forall (n0 : nat) (_ : @eq nat (S n) (Init.Nat.mul d (S n0))), le d (S n) *)
   intro q1.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: le d (Init.Nat.mul d (S q1)) *)
   apply le_n_nm.
Qed.

Lemma div_le : forall d n : nat, 0 < n -> Divides d n -> d <= n.
Proof.
(* Goal: forall (d n : Z) (_ : Z.gt d Z0), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r d)) (@eq Z n (Z.add (Z.mul q d) r)))) *)
   intros d n. case n.
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro. elim (lt_irrefl 0). assumption.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. apply div_le1. assumption.
Qed.

(** Divides with bounded ex quantifier. *)

Definition bDivides (d n : nat) :=
  n = 0 \/ (exists q : nat, q < S n /\ n = d * q).

Lemma divbdiv : forall n d : nat, Divides d n <-> bDivides d n.
Proof.
(* Goal: Divides a (Init.Nat.mul b c) *)
   unfold Divides in |- *.
(* Goal: or (bDivides d n) (not (bDivides d n)) *)
   unfold bDivides in |- *.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   case n.
(* Goal: forall _ : Divides (Z.abs_nat d) (Z.abs_nat x), or (ZDivides d x) (not (ZDivides d x)) *)
(* Goal: forall _ : not (Divides (Z.abs_nat d) (Z.abs_nat x)), or (ZDivides d x) (not (ZDivides d x)) *)
   left.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: forall _ : not (Divides (Z.abs_nat d) (Z.abs_nat x)), or (ZDivides d x) (not (ZDivides d x)) *)
   right.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (x : nat) (_ : @eq nat (S n0) (Init.Nat.mul d x)), @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul d q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   intro q.
(* Goal: forall _ : @eq nat (S n0) (Init.Nat.mul d q), @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul d q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   case d.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) O)) *)
(* Goal: forall (n : nat) (_ : @eq nat (S n0) (Init.Nat.mul (S n) q)), @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul (S n) q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   discriminate H0.
(* Goal: forall (n : nat) (_ : @eq nat (S n0) (Init.Nat.mul (S n) q)), @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul (S n) q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   intro d1.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => and (lt q (S (S n0))) (@eq nat (S n0) (Init.Nat.mul (S d1) q))) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   split with q.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: lt x N *)
(* Goal: gt d O *)
(* Goal: le d N *)
(* Goal: forall _ : lt N d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (le O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   unfold lt in |- *.
(* Goal: le (S q) (S (Init.Nat.mul (S d1) q)) *)
(* Goal: @eq nat (S n0) (Init.Nat.mul (S d1) q) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   apply le_n_S.
(* Goal: le q (Init.Nat.mul (S d1) q) *)
(* Goal: @eq nat (S n0) (Init.Nat.mul (S d1) q) *)
(* Goal: forall _ : or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   apply le_n_mn.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 0.
(* Goal: @eq nat O (Init.Nat.mul d O) *)
(* Goal: forall (_ : @ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))) (_ : @ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   rewrite <- (mult_n_O d).
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 0.
(* Goal: @eq nat O (Init.Nat.mul d O) *)
(* Goal: forall (_ : @ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))) (_ : @ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))), @ex nat (fun q : nat => @eq nat n (Init.Nat.mul d q)) *)
   rewrite <- (mult_n_O d).
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.add b c) *)
   elim H0.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul (S O) d) r)))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with x.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: Z.gt d Z0 *)
   assumption.
Qed.

(** Divides is decidable. *)

Lemma bdivdec : forall n d : nat, bDivides d n \/ ~ bDivides d n.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. unfold bDivides in |- *.
(* Goal: or (or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q))))) (not (or (@eq nat n O) (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))))) *)
   apply ordec.
(* Goal: or (@eq nat n (Init.Nat.mul d n0)) (not (@eq nat n (Init.Nat.mul d n0))) *)
   apply eqdec.
(* Goal: or (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q)))) (not (@ex nat (fun q : nat => and (lt q (S n)) (@eq nat n (Init.Nat.mul d q))))) *)
   apply (exdec (fun q : nat => n = d * q) (S n)).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. apply eqdec.
Qed.

Lemma divdec : forall n d : nat, Divides d n \/ ~ Divides d n.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. elim (divbdiv n d).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. elim (bdivdec n d).
(* Goal: forall _ : Divides (Z.abs_nat d) (Z.abs_nat x), or (ZDivides d x) (not (ZDivides d x)) *)
(* Goal: forall _ : not (Divides (Z.abs_nat d) (Z.abs_nat x)), or (ZDivides d x) (not (ZDivides d x)) *)
   left. apply (H0 H1).
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   right. intro. apply H1. apply (H H2).
Qed.

(** If d|n, then either d<sqrt(n) or the other divisor x<sqrt(n). *)

Theorem sqrdivbound :
 forall n d : nat,
 Divides d n ->
 exists x : nat, Divides x n /\ x * x <= n /\ (x = d \/ d * x = n).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun x : nat => and (Divides x n) (and (le (Init.Nat.mul x x) n) (or (@eq nat x d) (@eq nat (Init.Nat.mul d x) n)))) *)
   unfold Divides in H.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: @ex nat (fun x0 : nat => and (Divides x0 (Init.Nat.mul d x)) (and (le (Init.Nat.mul x0 x0) (Init.Nat.mul d x)) (or (@eq nat x0 d) (@eq nat (Init.Nat.mul d x0) (Init.Nat.mul d x))))) *)
   elim (sqrbound d x).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: Divides x (Init.Nat.mul d x) *)
(* Goal: and (le (Init.Nat.mul x x) (Init.Nat.mul d x)) (or (@eq nat x d) (@eq nat (Init.Nat.mul d x) (Init.Nat.mul d x))) *)
   split with d.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul (S O) d) r)))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with x.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall _ : Divides (Z.abs_nat d) (Z.abs_nat x), or (ZDivides d x) (not (ZDivides d x)) *)
(* Goal: forall _ : not (Divides (Z.abs_nat d) (Z.abs_nat x)), or (ZDivides d x) (not (ZDivides d x)) *)
   left.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul (S O) d) r)))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with x.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Divides x (Init.Nat.mul d x) *)
(* Goal: and (le (Init.Nat.mul x x) (Init.Nat.mul d x)) (or (@eq nat x d) (@eq nat (Init.Nat.mul d x) (Init.Nat.mul d x))) *)
   split with d.
(* Goal: @eq nat (Nat.mul (Nat.sub x0 x) d) (Init.Nat.mul d (Init.Nat.sub x0 x)) *)
   apply mult_comm.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall _ : not (Divides (Z.abs_nat d) (Z.abs_nat x)), or (ZDivides d x) (not (ZDivides d x)) *)
   right.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
Qed.


(**
   Division with remainder.
*)

Theorem div_rem :
 forall d n : nat,
 d > 0 -> exists q : nat, (exists r : nat, 0 <= r /\ r < d /\ n = q * d + r).
Proof.
(* Goal: forall (d n : Z) (_ : Z.gt d Z0), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r d)) (@eq Z n (Z.add (Z.mul q d) r)))) *)
   intros d n.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   apply (lt_wf_ind n). intros N IH. intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (le O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (le_or_lt d N).

   (* case d<=N *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (le O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : lt N d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (le O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (le_witness d N). intros x Hx.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim (IH x). intro q'. intros. elim H1. intro r'. intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2. intros. elim H4. intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with (S q'). split with r'.
(* Goal: Z.gt d Z0 *)
   split. assumption.
(* Goal: Z.gt d Z0 *)
   split. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *. rewrite <- Hx. rewrite (plus_assoc_reverse d (q' * d)).
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- H6. reflexivity.
(* Goal: lt x N *)
(* Goal: gt d O *)
(* Goal: le d N *)
(* Goal: forall _ : lt N d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (le O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   unfold lt in |- *. apply witness_le. split with (pred d). rewrite plus_Snm_nSm.
(* Goal: Z.gt d Z0 *)
   rewrite <- (S_pred d 0). rewrite plus_comm. assumption. assumption.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: Z.gt d Z0 *)
   assumption.

   (* case N<d *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 0. split with N.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split. apply le_O_n.
(* Goal: Z.gt d Z0 *)
   split. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *. reflexivity.
Qed.

Lemma div_rem0 :
 forall n d q r : nat, n = q * d + r -> r < d -> Divides d n -> r = 0.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H1.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @eq nat r O *)
   rewrite H2 in H.
(* Goal: @eq nat r O *)
   rewrite (mult_comm q d) in H.
(* Goal: @eq nat r O *)
   apply (le_diff0 (d * q) (d * x)).
(* Goal: le (Init.Nat.mul d x) (Init.Nat.mul d q) *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   apply le_mult_l.
(* Goal: le x q *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   apply le_S_n.
(* Goal: le (S x) (S q) *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   change (x < S q) in |- *.
(* Goal: lt x (S q) *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   apply simpl_lt_mult_l with d.
(* Goal: lt (Init.Nat.mul d x) (Init.Nat.mul d (S q)) *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   rewrite <- (mult_n_Sm d q).
(* Goal: lt (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) d) *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   replace (d * x) with (d * q + r).
(* Goal: lt (Init.Nat.add (Init.Nat.mul d q) r) (Init.Nat.add (Init.Nat.mul d q) d) *)
(* Goal: @eq nat (Init.Nat.mul d x) (Init.Nat.add (Init.Nat.mul d q) r) *)
   apply plus_lt_compat_l.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: Z.gt d Z0 *)
   assumption.
Qed.

Theorem notdiv_rem :
 forall d n : nat,
 0 < d ->
 ~ Divides d n ->
 exists q : nat, (exists r : nat, 0 < r /\ r < d /\ n = q * d + r).
Proof.
(* Goal: forall (d n : Z) (_ : Z.gt d Z0), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r d)) (@eq Z n (Z.add (Z.mul q d) r)))) *)
   intros d n.
(* Goal: forall (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (le_or_lt d n).
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: forall (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (le_lt_or_eq d n).
(* Goal: forall (_ : lt d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   apply (lt_wf_ind n).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros N IH. intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim (lt_witness d N). intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H3. intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (le_or_lt d x).
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (le_lt_or_eq d x).
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (divdec x d).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : not (Divides d x), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim H8.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : not (Divides d x), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite H9 in H4.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : not (Divides d x), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite plus_comm in H4.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : not (Divides d x), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite mult_n_Sm in H4.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2.
(* Goal: Divides d N *)
(* Goal: forall _ : not (Divides d x), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with (S x0).
   symmetry  in |- *.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim (IH x).
(* Goal: forall (x0 : nat) (_ : @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat x (Init.Nat.add (Init.Nat.mul x0 d) r))))), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   intro q'.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim H9.
(* Goal: forall (x0 : nat) (_ : and (lt O x0) (and (lt x0 d) (@eq nat x (Init.Nat.add (Init.Nat.mul q' d) x0)))), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   intro r'.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim H10.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   elim H12.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with (S q').
(* Goal: @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul (S q') d) r)))) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with r'.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: @eq nat N (Init.Nat.add (Init.Nat.add d (Init.Nat.mul q' d)) r') *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite plus_assoc_reverse.
(* Goal: @eq nat N (Init.Nat.add d (Init.Nat.add (Init.Nat.mul q' d) r')) *)
(* Goal: lt x N *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite <- H14.
   symmetry  in |- *.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: @eq nat N (Nat.add d d) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite <- H4.
(* Goal: lt x (Init.Nat.add d x) *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   pattern x at 1 in |- *.
(* Goal: (fun n : nat => lt n (Init.Nat.add d x)) x *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   replace x with (0 + x).
(* Goal: lt (Init.Nat.add O x) (Init.Nat.add d x) *)
(* Goal: @eq nat (Init.Nat.add O x) x *)
(* Goal: lt d x *)
(* Goal: lt O d *)
(* Goal: not (Divides d x) *)
(* Goal: forall _ : @eq nat d x, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   apply plus_lt_compat_r.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2.
(* Goal: Divides d N *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 2.
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) (Nat.mul x0 d)) *)
   rewrite mult_comm.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: @eq nat n (Nat.add d O) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite <- (plus_n_O d).
(* Goal: @eq nat N (Nat.add d d) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite <- H4.
(* Goal: @eq nat (Init.Nat.add d x) (Nat.add d d) *)
(* Goal: le d x *)
(* Goal: forall _ : lt x d, @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite H7.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: Divides d n *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 1.
(* Goal: @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat N (Init.Nat.add (Init.Nat.mul (S O) d) r)))) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with x.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: @eq nat n (Nat.add d O) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite <- (plus_n_O d).
(* Goal: @eq nat N (Init.Nat.add d x) *)
(* Goal: lt d N *)
(* Goal: forall (_ : @eq nat d n) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite H4.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2.
(* Goal: Divides d n *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 1.
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) (Nat.mul x0 d)) *)
   rewrite mult_comm.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: @eq nat n (Nat.add d O) *)
(* Goal: le d n *)
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   rewrite <- (plus_n_O d).
   symmetry  in |- *.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: forall (_ : lt n d) (_ : lt O d) (_ : not (Divides d n)), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat n (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   case n.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H1.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 0.
(* Goal: @eq nat O (Init.Nat.mul d O) *)
(* Goal: forall (n : nat) (_ : lt (S n) d) (_ : lt O d) (_ : not (Divides d (S n))), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   apply mult_n_O.
(* Goal: forall (n : nat) (_ : lt (S n) d) (_ : lt O d) (_ : not (Divides d (S n))), @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   intro n1.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: @ex nat (fun q : nat => @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul q d) r))))) *)
   split with 0.
(* Goal: @ex nat (fun r : nat => and (lt O r) (and (lt r d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul O d) r)))) *)
   split with (S n1).
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: lt O (S n1) *)
(* Goal: and (lt (S n1) d) (@eq nat (S n1) (Init.Nat.add (Init.Nat.mul O d) (S n1))) *)
   apply lt_O_Sn.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *. reflexivity.
Qed.

(** Compatibility results. *)

Lemma div_plus_compat :
 forall a b c : nat, Divides a b -> Divides a c -> Divides a (b + c).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H. intro x. intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H0. intro y. intros.
(* Goal: Divides a (Init.Nat.add b c) *)
   split with (x + y).
(* Goal: @eq Z (Z.add b c) (Z.mul a (Z.add x y)) *)
   rewrite H1. rewrite H2. symmetry  in |- *.
(* Goal: @eq nat (Nat.mul (Init.Nat.add x y) a) (Init.Nat.add (Nat.mul x a) (Init.Nat.mul a y)) *)
   rewrite (mult_comm a). rewrite (mult_comm a). rewrite (mult_comm a).
(* Goal: @eq nat (Nat.mul (Init.Nat.add x y) a) (Init.Nat.add (Nat.mul x a) (Nat.mul y a)) *)
   apply mult_plus_distr_r.
Qed.

Lemma div_minus_compat :
 forall a b d : nat, Divides d a -> Divides d b -> Divides d (a - b).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. elim H. elim H0. intros.
(* Goal: Divides a (Init.Nat.mul b c) *)
   unfold Divides in |- *. rewrite H1. rewrite H2.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub (Nat.mul x0 d) (Init.Nat.mul d x)) (Init.Nat.mul d q)) *)
   rewrite (mult_comm d).
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub (Nat.mul x0 d) (Init.Nat.mul d x)) (Init.Nat.mul d q)) *)
   rewrite (mult_comm d).
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub (Nat.mul x0 d) (Nat.mul x d)) (Init.Nat.mul d q)) *)
   rewrite <- mult_minus_distr_r.
(* Goal: @ex nat (fun q : nat => @eq nat (Nat.mul (Nat.sub x0 x) d) (Init.Nat.mul d q)) *)
   split with (x0 - x).
(* Goal: @eq nat (Nat.mul (Nat.sub x0 x) d) (Init.Nat.mul d (Init.Nat.sub x0 x)) *)
   apply mult_comm.
Qed.

Lemma div_mult_compat_l :
 forall a b c : nat, Divides a b -> Divides a (b * c).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (x : Z) (_ : @eq Z b (Z.mul a x)), ZDivides a (Z.mul b c) *)
   intro x.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: Divides a (Init.Nat.mul b c) *)
   unfold Divides in |- *.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.mul (Init.Nat.mul a x) c) (Init.Nat.mul a q)) *)
   split with (x * c).
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a x) c) (Init.Nat.mul a (Init.Nat.mul x c)) *)
   rewrite mult_assoc.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
Qed.

Lemma div_absexp_compat :
 forall (b : Z) (d : nat),
 Divides d (Zabs_nat b) -> forall n : nat, Divides d (Zabs_nat (Exp b (S n))).
Proof.
(* Goal: ZDivides a (Z.mul b c) *)
   intros b d H. elim H. intros k Hk. simple induction n.
(* Goal: Divides d (Z.abs_nat (Exp b (S O))) *)
(* Goal: forall (n : nat) (_ : Divides d (Z.abs_nat (Exp b (S n)))), Divides d (Z.abs_nat (Exp b (S (S n)))) *)
   split with k.
(* Goal: @eq nat (Z.abs_nat (Exp b (S O))) (Init.Nat.mul d k) *)
(* Goal: forall (n : nat) (_ : Divides d (Z.abs_nat (Exp b (S n)))), Divides d (Z.abs_nat (Exp b (S (S n)))) *)
   rewrite <- Hk.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: Divides d (Z.abs_nat (Z.mul b (Exp b (S m)))) *)
(* Goal: @eq Z (Z.mul b (Exp b (S m))) (Exp b (S (S m))) *)
   rewrite abs_mult.
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) (Nat.mul x0 d)) *)
   rewrite mult_comm.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *.
(* Goal: @eq nat (Nat.add (Z.abs_nat b) O) (Z.abs_nat b) *)
(* Goal: forall (n : nat) (_ : Divides d (Z.abs_nat (Exp b (S n)))), Divides d (Z.abs_nat (Exp b (S (S n)))) *)
   rewrite <- plus_n_O.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: forall (n : nat) (_ : Divides d (Z.abs_nat (Exp b (S n)))), Divides d (Z.abs_nat (Exp b (S (S n)))) *)
   intros m IH.
(* Goal: Divides d (Z.abs_nat (Exp b (S (S m)))) *)
   replace (Exp b (S (S m))) with (b * Exp b (S m))%Z.
(* Goal: Divides d (Z.abs_nat (Z.mul b (Exp b (S m)))) *)
(* Goal: @eq Z (Z.mul b (Exp b (S m))) (Exp b (S (S m))) *)
   rewrite abs_mult.
(* Goal: Divides d (Init.Nat.mul (Z.abs_nat b) (Z.abs_nat (Exp b (S m)))) *)
(* Goal: @eq Z (Z.mul b (Exp b (S m))) (Exp b (S (S m))) *)
   apply div_mult_compat_l.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   simpl in |- *. reflexivity.
Qed.

Lemma div_plus_r :
 forall a b d : nat, Divides d a -> Divides d (a + b) -> Divides d b.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros. elim H. elim H0. intros.
(* Goal: Divides d b *)
   split with (x - x0).
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) (Nat.mul x0 d)) *)
   rewrite mult_comm.
(* Goal: @eq nat b (Nat.mul (Init.Nat.sub x x0) d) *)
   rewrite mult_minus_distr_r.
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) (Nat.mul x0 d)) *)
   rewrite mult_comm.
(* Goal: @eq Z b (Z.sub (Z.mul d x) (Z.mul x0 d)) *)
   rewrite <- H1.
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) (Nat.mul x0 d)) *)
   rewrite mult_comm.
(* Goal: @eq Z b (Z.sub (Z.add a b) (Z.mul d x0)) *)
   rewrite <- H2.
(* Goal: @eq nat b (Nat.sub (Init.Nat.add a b) a) *)
   rewrite minus_plus.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
Qed.

(** * Division on Z. *)

Definition ZDivides (x y : Z) : Prop := exists q : Z, y = (x * q)%Z.

Lemma zdivdiv :
 forall a b : Z, ZDivides a b -> Divides (Zabs_nat a) (Zabs_nat b).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (x : nat) (_ : @eq nat (Z.abs_nat b) (Init.Nat.mul (Z.abs_nat a) x)), ZDivides a b *)
   intros d Hd.
(* Goal: Divides (Z.abs_nat a) (Z.abs_nat b) *)
   exists (Zabs_nat d).
(* Goal: @eq Z (Z.of_nat (Z.abs_nat b)) (Z.of_nat (Init.Nat.mul (Z.abs_nat a) d)) *)
(* Goal: Z.lt a Z0 *)
(* Goal: Z.lt b Z0 *)
   rewrite Hd.
(* Goal: @eq nat (Z.abs_nat (Z.mul a d)) (Init.Nat.mul (Z.abs_nat a) (Z.abs_nat d)) *)
   apply abs_mult.
Qed.

Lemma divzdiv :
 forall a b : Z, Divides (Zabs_nat a) (Zabs_nat b) -> ZDivides a b.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (x : nat) (_ : @eq nat (Z.abs_nat b) (Init.Nat.mul (Z.abs_nat a) x)), ZDivides a b *)
   intros d Hd.
(* Goal: ZDivides a b *)
   elim (Zle_or_lt 0 a).
(* Goal: forall _ : Z.lt a Z0, ZDivides a b *)
   elim (Zle_or_lt 0 b).

   (* case 0<=b, a<=b *)
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a b *)
   exists (Z_of_nat d).
(* Goal: @eq Z b (Z.mul (Z.opp (Z.of_nat (Z.abs_nat a))) (Z.opp (Z.of_nat d))) *)
(* Goal: Z.lt a Z0 *)
(* Goal: forall (_ : Z.lt b Z0) (_ : Z.lt a Z0), ZDivides a b *)
   rewrite <- (inj_abs_pos b).
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat b))) (Z.mul a (Z.opp (Z.of_nat d))) *)
(* Goal: Z.lt b Z0 *)
(* Goal: forall _ : Z.lt a Z0, ZDivides a b *)
   rewrite <- (inj_abs_pos a).
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Hd. reflexivity.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. assumption.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. assumption.

   (* case b<0, 0<=a *)
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a b *)
(* Goal: forall (_ : Z.lt b Z0) (_ : Z.lt a Z0), ZDivides a b *)
   exists (- Z_of_nat d)%Z.
(* Goal: @eq Z b (Z.mul a (Z.of_nat d)) *)
   rewrite <- (Zopp_involutive b).
(* Goal: @eq Z (Z.opp (Z.opp b)) (Z.mul (Z.opp (Z.opp a)) (Z.of_nat d)) *)
   rewrite <- (inj_abs_neg b).
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat b))) (Z.mul a (Z.opp (Z.of_nat d))) *)
(* Goal: Z.lt b Z0 *)
(* Goal: forall _ : Z.lt a Z0, ZDivides a b *)
   rewrite <- (inj_abs_pos a).
(* Goal: @eq Z b (Z.sub (Z.add a b) (Z.mul x0 d)) *)
   rewrite Zmult_comm. rewrite Zopp_mult_distr_l_reverse. rewrite Zmult_comm.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat b))) (Z.opp (Z.of_nat (Init.Nat.mul (Z.abs_nat a) d))) *)
(* Goal: Z.lt a Z0 *)
(* Goal: Z.lt b Z0 *)
   apply (f_equal (A:=Z)).
(* Goal: @eq Z (Z.of_nat (Z.abs_nat b)) (Z.of_nat (Init.Nat.mul (Z.abs_nat a) d)) *)
(* Goal: Z.lt a Z0 *)
(* Goal: Z.lt b Z0 *)
   rewrite Hd.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. assumption.
(* Goal: Z.gt d Z0 *)
   assumption.

(* Goal: forall _ : Z.lt a Z0, ZDivides a b *)
   elim (Zle_or_lt 0 b).

   (* case 0<=b, a<0 *)
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a b *)
(* Goal: forall (_ : Z.lt b Z0) (_ : Z.lt a Z0), ZDivides a b *)
   exists (- Z_of_nat d)%Z.
(* Goal: @eq Z (Z.opp (Z.opp b)) (Z.mul a (Z.of_nat d)) *)
   rewrite <- (Zopp_involutive a).
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat b))) (Z.mul (Z.opp (Z.opp a)) (Z.of_nat d)) *)
(* Goal: Z.lt b Z0 *)
   rewrite <- (inj_abs_neg a).
(* Goal: @eq Z b (Z.mul (Z.opp (Z.of_nat (Z.abs_nat a))) (Z.opp (Z.of_nat d))) *)
(* Goal: Z.lt a Z0 *)
(* Goal: forall (_ : Z.lt b Z0) (_ : Z.lt a Z0), ZDivides a b *)
   rewrite <- (inj_abs_pos b).
(* Goal: @eq Z (Z.of_nat (Z.abs_nat b)) (Z.mul (Z.opp (Z.of_nat (Z.abs_nat a))) (Z.opp (Z.of_nat d))) *)
(* Goal: Z.ge b Z0 *)
(* Goal: Z.lt a Z0 *)
(* Goal: forall (_ : Z.lt b Z0) (_ : Z.lt a Z0), ZDivides a b *)
   rewrite Zmult_opp_opp.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z (Z.of_nat (Z.abs_nat b)) (Z.of_nat (Init.Nat.mul (Z.abs_nat a) d)) *)
(* Goal: Z.lt a Z0 *)
(* Goal: Z.lt b Z0 *)
   rewrite Hd.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. assumption.
(* Goal: Z.gt d Z0 *)
   assumption.

   (* case b<0, a<0 *)
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a b *)
   exists (Z_of_nat d).
(* Goal: @eq Z b (Z.mul a (Z.of_nat d)) *)
   rewrite <- (Zopp_involutive b).
(* Goal: @eq Z (Z.opp (Z.opp b)) (Z.mul a (Z.of_nat d)) *)
   rewrite <- (Zopp_involutive a).
(* Goal: @eq Z (Z.opp (Z.opp b)) (Z.mul (Z.opp (Z.opp a)) (Z.of_nat d)) *)
   rewrite <- (inj_abs_neg b).
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat b))) (Z.mul (Z.opp (Z.opp a)) (Z.of_nat d)) *)
(* Goal: Z.lt b Z0 *)
   rewrite <- (inj_abs_neg a).
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat b))) (Z.opp (Z.of_nat (Init.Nat.mul (Z.abs_nat a) d))) *)
(* Goal: Z.lt a Z0 *)
(* Goal: Z.lt b Z0 *)
   apply (f_equal (A:=Z)).
(* Goal: @eq Z (Z.of_nat (Z.abs_nat b)) (Z.of_nat (Init.Nat.mul (Z.abs_nat a) d)) *)
(* Goal: Z.lt a Z0 *)
(* Goal: Z.lt b Z0 *)
   rewrite Hd.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
(* Goal: Z.gt d Z0 *)
   assumption.
(* Goal: Z.gt d Z0 *)
   assumption.
Qed.

Lemma zdivdec : forall x d : Z, ZDivides d x \/ ~ ZDivides d x. 
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: or (ZDivides d x) (not (ZDivides d x)) *)
   elim (divdec (Zabs_nat x) (Zabs_nat d)).
(* Goal: Z.gt d Z0 *)
   left. apply divzdiv. assumption.
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   right. intro. apply H. apply zdivdiv. assumption.
Qed.

Lemma zdiv_plus_r :
 forall a b d : Z, ZDivides d a -> ZDivides d (a + b) -> ZDivides d b.
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: ZDivides a (Z.add b c) *)
   elim H0.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides d b *)
   split with (x - x0)%Z.
(* Goal: @eq Z b (Z.sub (Z.add a b) (Z.mul x0 d)) *)
   rewrite Zmult_comm.
(* Goal: @eq Z b (Z.mul (Z.sub x x0) d) *)
   rewrite Zmult_minus_distr_r.
(* Goal: @eq Z b (Z.sub (Z.add a b) (Z.mul x0 d)) *)
   rewrite Zmult_comm.
(* Goal: @eq Z b (Z.sub (Z.mul d x) (Z.mul x0 d)) *)
   rewrite <- H1.
(* Goal: @eq Z b (Z.sub (Z.add a b) (Z.mul x0 d)) *)
   rewrite Zmult_comm.
(* Goal: @eq Z b (Z.sub (Z.add a b) (Z.mul d x0)) *)
   rewrite <- H2.
(* Goal: @eq Z b (Z.sub (Z.add a b) a) *)
   rewrite Zminus_plus.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
Qed.

Lemma zdiv_plus_compat :
 forall a b c : Z, ZDivides a b -> ZDivides a c -> ZDivides a (b + c).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H. intro x. intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H0. intro y. intros.
(* Goal: ZDivides a (Z.add b c) *)
   split with (x + y)%Z.
(* Goal: @eq Z (Z.add b c) (Z.mul a (Z.add x y)) *)
   rewrite H1. rewrite H2. symmetry  in |- *.
(* Goal: @eq Z (Z.mul (Z.add x y) a) (Z.add (Z.mul x a) (Z.mul a y)) *)
   rewrite (Zmult_comm a). rewrite (Zmult_comm a). rewrite (Zmult_comm a).
(* Goal: @eq Z (Z.mul (Z.add x y) a) (Z.add (Z.mul x a) (Z.mul y a)) *)
   apply Zmult_plus_distr_l.
Qed.

Lemma zdiv_mult_compat_l :
 forall a b c : Z, ZDivides a b -> ZDivides a (b * c).
Proof.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   elim H.
(* Goal: forall (x : Z) (_ : @eq Z b (Z.mul a x)), ZDivides a (Z.mul b c) *)
   intro x.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros.
(* Goal: ZDivides a (Z.mul b c) *)
   unfold ZDivides in |- *.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul b c) (Z.mul a q)) *)
   rewrite H0.
(* Goal: @ex Z (fun q : Z => @eq Z (Z.mul (Z.mul a x) c) (Z.mul a q)) *)
   split with (x * c)%Z.
(* Goal: @eq Z (Z.mul (Z.mul a x) c) (Z.mul a (Z.mul x c)) *)
   rewrite Zmult_assoc.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   reflexivity.
Qed.

Theorem zdiv_rem :
 forall d n : Z,
 (d > 0)%Z ->
 exists q : Z, (exists r : Z, (0 <= r < d)%Z /\ n = (q * d + r)%Z).
Proof.
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intros d n. intro.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r d)) (@eq Z n (Z.add (Z.mul q d) r)))) *)
   elim (Zle_or_lt 0 n).

   (* case 0<=n *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro. rewrite <- (inj_abs_pos d). rewrite <- (inj_abs_pos n).
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim (div_rem (Zabs_nat d) (Zabs_nat n)).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro qn. intros. elim H1. intro rn. intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2. intros. elim H4. intros.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.of_nat (Z.abs_nat n)) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge d Z0 *)
(* Goal: forall _ : Z.lt n Z0, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r d)) (@eq Z n (Z.add (Z.mul q d) r)))) *)
   split with (Z_of_nat qn). split with (Z_of_nat rn).
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split. split. change (Z_of_nat 0 <= Z_of_nat rn)%Z in |- *.
(* Goal: le O rn *)
(* Goal: Z.lt (Z.of_nat rn) (Z.of_nat (Z.abs_nat d)) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   apply Znat.inj_le. apply le_O_n.
(* Goal: Z.gt d Z0 *)
   apply Znat.inj_lt. assumption.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- Znat.inj_mult. rewrite <- Znat.inj_plus. apply Znat.inj_eq.
(* Goal: Z.gt d Z0 *)
   assumption. change (Zabs_nat d > Zabs_nat 0) in |- *. apply gtzgt.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   apply Zlt_le_weak. apply Zgt_lt. assumption. apply Zeq_le. reflexivity.
(* Goal: Z.gt d Z0 *)
   assumption. apply Zle_ge. assumption. apply Zle_ge.
(* Goal: Z.gt d Z0 *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.

   (* case n<0 *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro. rewrite <- (inj_abs_pos d).
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z n (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: Z.ge d Z0 *)
   replace n with (- - n)%Z. rewrite <- (inj_abs_neg n).
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim (div_rem (Zabs_nat d) (Zabs_nat n)).
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro qn. intros. elim H1. intro rn. intros.
(* Goal: forall (_ : lt rn (Z.abs_nat d)) (_ : @eq nat (Z.abs_nat n) (Init.Nat.add (Init.Nat.mul qn (Z.abs_nat d)) rn)), @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim H2. intros. elim H4. intros.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   elim (le_lt_or_eq 0 rn).

   (* case 0<rn *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro. split with (- Z_of_nat (S qn))%Z. split with (d - Z_of_nat rn)%Z.
(* Goal: and (Z.le Z0 Z0) (Z.lt Z0 (Z.of_nat (Z.abs_nat d))) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split. split. rewrite <- (inj_abs_pos d). apply Zle_minus. apply Znat.inj_le.
(* Goal: Z.gt d Z0 *)
   apply lt_le_weak. assumption.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: Z.lt (Z.sub d (Z.of_nat rn)) (Z.of_nat (Z.abs_nat d)) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat (S qn))) (Z.of_nat (Z.abs_nat d))) (Z.sub d (Z.of_nat rn))) *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite inj_abs_pos. apply Zplus_lt_reg_l with (Z_of_nat rn).
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.add (Z.opp (Z.of_nat (Init.Nat.mul qn (Z.abs_nat d)))) (Z.opp d)) (Z.sub d (Z.of_nat rn))) *)
(* Goal: Z.ge d Z0 *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   unfold Zminus in |- *. rewrite (Zplus_comm d).
(* Goal: Z.lt (Z.add (Z.of_nat rn) (Z.add (Z.opp (Z.of_nat rn)) d)) (Z.add (Z.of_nat rn) d) *)
(* Goal: Z.ge d Z0 *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat (S qn))) (Z.of_nat (Z.abs_nat d))) (Z.sub d (Z.of_nat rn))) *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite (Zplus_assoc (Z_of_nat rn)).
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Zplus_opp_r. simpl in |- *. change (0 + d < Z_of_nat rn + d)%Z in |- *.
(* Goal: Z.lt (Z.add Z0 d) (Z.add (Z.of_nat rn) d) *)
(* Goal: Z.ge d Z0 *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat (S qn))) (Z.of_nat (Z.abs_nat d))) (Z.sub d (Z.of_nat rn))) *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Zplus_comm. rewrite (Zplus_comm (Z_of_nat rn)). apply Zplus_lt_compat_l.
(* Goal: Z.gt d Z0 *)
   change (Z_of_nat 0 < Z_of_nat rn)%Z in |- *. apply Znat.inj_lt. assumption.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Znat.inj_S. unfold Zsucc in |- *. rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Zmult_plus_distr_l. rewrite <- Znat.inj_mult. rewrite Zmult_1_l.
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.opp (Z.add (Z.of_nat (Init.Nat.mul qn (Z.abs_nat d))) (Z.of_nat (Z.abs_nat d)))) (Z.sub d (Z.of_nat rn))) *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite (inj_abs_pos d). rewrite Zopp_plus_distr.
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.add (Z.opp (Z.of_nat (Init.Nat.mul qn (Z.abs_nat d)))) (Z.opp d)) (Z.sub d (Z.of_nat rn))) *)
(* Goal: Z.ge d Z0 *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   unfold Zminus in |- *. rewrite Zplus_assoc_reverse. rewrite (Zplus_assoc (- d)).
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Zplus_opp_l. simpl in |- *. rewrite <- Zopp_plus_distr. rewrite <- Znat.inj_plus.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- H6. reflexivity.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.

   (* case 0=rn *)
(* Goal: forall _ : @eq nat O rn, @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   intro.
(* Goal: @ex Z (fun q : Z => @ex Z (fun r : Z => and (and (Z.le Z0 r) (Z.lt r (Z.of_nat (Z.abs_nat d)))) (@eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul q (Z.of_nat (Z.abs_nat d))) r)))) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split with (- Z_of_nat qn)%Z. split with 0%Z.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   split. split. unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: Z.lt Z0 (Z.of_nat (Z.abs_nat d)) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   apply Zle_lt_trans with (Z_of_nat rn).
(* Goal: le O rn *)
(* Goal: Z.lt (Z.of_nat rn) (Z.of_nat (Z.abs_nat d)) *)
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   change (Z_of_nat 0 <= Z_of_nat rn)%Z in |- *. apply Znat.inj_le. apply le_O_n.
(* Goal: Z.gt d Z0 *)
   apply Znat.inj_lt. assumption.
(* Goal: @eq Z (Z.opp (Z.of_nat (Z.abs_nat n))) (Z.add (Z.mul (Z.opp (Z.of_nat qn)) (Z.of_nat (Z.abs_nat d))) Z0) *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- Zplus_0_r_reverse. rewrite inj_abs_neg.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.mul (Z.of_nat qn) (Z.of_nat (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite Zopp_mult_distr_l_reverse. rewrite <- Znat.inj_mult.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.of_nat (Init.Nat.mul qn (Z.abs_nat d)))) *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite <- H7 in H6. rewrite <- plus_n_O in H6. rewrite <- H6.
(* Goal: @eq Z (Z.opp (Z.opp n)) (Z.opp (Z.opp n)) *)
(* Goal: Z.lt n Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: le O rn *)
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   rewrite inj_abs_neg. reflexivity.
(* Goal: Z.gt d Z0 *)
   assumption. assumption. assumption.
(* Goal: gt (Z.abs_nat d) O *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   change (Zabs_nat d > Zabs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak.
(* Goal: Z.gt d Z0 *)
   apply Zgt_lt. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt d Z0 *)
(* Goal: Z.lt n Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: Z.gt d Z0 *)
   assumption. assumption.
(* Goal: @eq Z (Z.opp (Z.opp n)) n *)
(* Goal: Z.ge d Z0 *)
   apply Zopp_involutive.
(* Goal: Z.gt d Z0 *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
Qed.
