(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  Zdiv.v                                  *)
(****************************************************************************)
Require Export Zbase.
Require Export Zadd.
Require Export Zmult.
Require Export Zle.
Require Export Euclid.

Unset Standard Proposition Elimination Names.

(********************)
Definition is_diveuclZ (a b q r : Z) :=
  b <> OZ /\ leZ OZ r /\ ltZ r (absZ b) /\ a = addZ (multZ b q) r.

(***************************)
Inductive diveuclZ (a b : Z) : Set :=
    divexZ : forall q r : Z, is_diveuclZ a b q r -> diveuclZ a b.

(************************)
Lemma divZ : forall a b : Z, b <> OZ -> diveuclZ a b.

Proof.
(* Goal: forall (a b : Z) (_ : not (@eq Z b OZ)), diveuclZ a b *)
  intros a b; case b; intros. elim H; reflexivity.
(* Goal: diveuclZ a (neg n) *)
  case a; intros. apply (divexZ OZ (pos n) OZ OZ).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. discriminate. split. exact I. split.
(* Goal: ltZ OZ (absZ (neg n)) *)
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (posOZ q)) OZ) *)
(* Goal: diveuclZ (neg n0) (neg n) *)
  exact (le_O_n n). rewrite (mult_OZ (pos n)).
(* Goal: @eq Z OZ (addZ OZ OZ) *)
(* Goal: diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  reflexivity.
(* Goal: diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  elim (eucl_dev (S n) (gt_Sn_O n) (S n0)). intros.
(* Goal: diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  apply (divexZ (pos n0) (pos n) (posOZ q) (posOZ r)).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. discriminate. split. apply (tech_posOZ_pos r).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. unfold ltZ in |- *; rewrite (tech_succ_posOZ r).
(* Goal: leZ (pos r) (absZ (pos n)) *)
(* Goal: @eq Z (pos n0) (addZ (multZ (pos n) (posOZ q)) (posOZ r)) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  exact (gt_S_le r n g). exact (tech_div1 n0 n q r e).
(* Goal: forall (q r : nat) (_ : gt (S n) r) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)), diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  elim (eucl_dev (S n) (gt_Sn_O n) (S n0)); intros.
(* Goal: diveuclZ (neg n0) (neg n) *)
  case (eq_gt_O_dec r); intro. 
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  apply (divexZ (neg n0) (pos n) (negOZ q) OZ). split.
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  discriminate. split. exact I. split. exact (le_O_n n).
(* Goal: @eq Z (neg n0) (addZ (multZ (pos n) (negOZ q)) OZ) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  rewrite (add_OZ (multZ (pos n) (negOZ q))).
(* Goal: @eq Z (neg n0) (multZ (pos n) (negOZ q)) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  apply (tech_div2 n0 n q). rewrite e; rewrite e0; auto with arith.
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  apply (divexZ (neg n0) (pos n) (neg q) (pos (n - r))).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. discriminate. split. exact I. split.
(* Goal: ltZ (pos (Init.Nat.sub n r)) (absZ (neg n)) *)
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
  exact (lt_le_S (n - r) n (lt_minus n r (gt_S_le r n g) g0)).
(* Goal: diveuclZ a (neg n) *)
  exact (tech_div3 n0 n q r e g). case a; intros.
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  apply (divexZ OZ (neg n) OZ OZ). split. discriminate.
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. exact I. split. exact (le_O_n n).
(* Goal: @eq Z OZ (addZ OZ OZ) *)
(* Goal: diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  rewrite (mult_OZ (neg n)); reflexivity.
(* Goal: forall (q r : nat) (_ : gt (S n) r) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)), diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  elim (eucl_dev (S n) (gt_Sn_O n) (S n0)); intros.
(* Goal: diveuclZ (pos n0) (neg n) *)
(* Goal: diveuclZ (neg n0) (neg n) *)
  apply (divexZ (pos n0) (neg n) (negOZ q) (posOZ r)).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. discriminate. split. apply (tech_posOZ_pos r).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. unfold ltZ in |- *; rewrite (tech_succ_posOZ r); exact (gt_S_le r n g).
(* Goal: forall (q r : nat) (_ : gt (S n) r) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)), diveuclZ (pos n0) (pos n) *)
(* Goal: diveuclZ (neg n0) (pos n) *)
(* Goal: diveuclZ a (neg n) *)
  exact (tech_div4 n0 n q r e). elim (eucl_dev (S n) (gt_Sn_O n) (S n0)); intros. case (eq_gt_O_dec r); intro. 
(* Goal: diveuclZ (neg n0) (neg n) *)
(* Goal: diveuclZ (neg n0) (neg n) *)
  apply (divexZ (neg n0) (neg n) (posOZ q) OZ). unfold is_diveuclZ in |- *.
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. discriminate. split. exact I. split. exact (le_O_n n).
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (posOZ q)) OZ) *)
(* Goal: diveuclZ (neg n0) (neg n) *)
  rewrite (add_OZ (multZ (neg n) (posOZ q))). apply (tech_div5 n0 n q).
(* Goal: @eq nat (S n0) (Init.Nat.mul q (S n)) *)
(* Goal: diveuclZ (neg n0) (neg n) *)
  rewrite e; rewrite e0; auto with arith.
(* Goal: diveuclZ (neg n0) (neg n) *)
  apply (divexZ (neg n0) (neg n) (pos q) (pos (n - r))).
(* Goal: and (ltZ (pos (Init.Nat.sub n r)) (absZ (neg n))) (@eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r)))) *)
  split. discriminate. split. exact I. split.
(* Goal: ltZ (pos (Init.Nat.sub n r)) (absZ (neg n)) *)
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
  exact (lt_le_S (n - r) n (lt_minus n r (gt_S_le r n g) g0)).
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
  exact (tech_div6 n0 n q r e g).
Qed.
