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



Require Import ZArith.
Require Import ZArithRing.
Require Import Zcomplements.

Unset Standard Proposition Elimination Names.

(** Divisibility *)

Inductive divide (a b : Z) : Prop :=
    divide_intro : forall q : Z, b = (q * a)%Z -> divide a b.

Notation "( x | y )" := (divide x y) (at level 0) : Z_scope.

Local Open Scope Z_scope.


(** Results *)

Lemma divide_refl : forall a : Z, (a | a).
Proof.
(* Goal: forall a : Z, divide a a *)
intros; apply divide_intro with 1; ring.
Qed.

Lemma one_divide : forall a : Z, (1 | a).
Proof.
(* Goal: forall a : Z, divide (Zpos xH) a *)
intros; apply divide_intro with a; ring.
Qed.

Lemma divide_0 : forall a : Z, (a | 0).
Proof.
(* Goal: forall a : Z, divide a Z0 *)
intros; apply divide_intro with 0; ring.
Qed.

Hint Resolve divide_refl one_divide divide_0.

Lemma divide_mult_left : forall a b c : Z, (a | b) -> (c * a | c * b).
Proof.
(* Goal: forall (a b c : Z) (_ : divide a b), divide (Z.mul c a) (Z.mul c b) *)
simple induction 1; intros; apply divide_intro with q.
(* Goal: @eq Z (Z.mul (Z.opp q) a) (Z.opp b) *)
(* Goal: Z.le a b *)
(* Goal: Z.le a b *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H0; ring.
Qed.

Lemma divide_mult_right : forall a b c : Z, (a | b) -> (a * c | b * c).
Proof.
(* Goal: forall (a b c : Z) (_ : divide a b), divide (Z.mul a c) (Z.mul b c) *)
intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c).
(* Goal: forall _ : divide a b, divide (Z.mul c a) (Z.mul c b) *)
apply divide_mult_left; trivial.
Qed.

Hint Resolve divide_mult_left divide_mult_right.

Lemma divide_plus : forall a b c : Z, (a | b) -> (a | c) -> (a | b + c).
Proof.
(* Goal: forall (a b c : Z) (_ : divide a b) (_ : divide a c), divide a (Z.sub b c) *)
simple induction 1; intros q Hq; simple induction 1; intros q' Hq'.
(* Goal: divide a (Z.add b c) *)
apply divide_intro with (q + q').
(* Goal: @eq Z (Z.sub b c) (Z.mul (Z.sub q q') a) *)
rewrite Hq; rewrite Hq'; ring.
Qed.

Lemma divide_opp : forall a b : Z, (a | b) -> (a | - b).
Proof.
(* Goal: forall (a b : Z) (_ : divide a b), divide (Z.opp a) b *)
simple induction 1; intros; apply divide_intro with (- q).
(* Goal: @eq Z (Z.mul (Z.opp q) a) (Z.opp b) *)
(* Goal: Z.le a b *)
(* Goal: Z.le a b *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H0; ring.
Qed.

Lemma divide_opp_rev : forall a b : Z, (a | - b) -> (a | b).
Proof.
(* Goal: forall (a b : Z) (_ : divide a (Z.opp b)), divide a b *)
intros; replace b with (- - b). apply divide_opp; trivial. ring.
Qed.

Lemma divide_opp_left : forall a b : Z, (a | b) -> (- a | b).
Proof.
(* Goal: forall (a b : Z) (_ : divide a b), divide (Z.opp a) b *)
simple induction 1; intros; apply divide_intro with (- q).
(* Goal: @eq Z (Z.mul (Z.opp q) a) (Z.opp b) *)
(* Goal: Z.le a b *)
(* Goal: Z.le a b *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H0; ring.
Qed.

Lemma divide_opp_left_rev : forall a b : Z, (- a | b) -> (a | b).
Proof.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
intros; replace a with (- - a). apply divide_opp_left; trivial. ring.
Qed.

Lemma divide_minus : forall a b c : Z, (a | b) -> (a | c) -> (a | b - c).
Proof.
(* Goal: forall (a b c : Z) (_ : divide a b) (_ : divide a c), divide a (Z.sub b c) *)
simple induction 1; intros q Hq; simple induction 1; intros q' Hq'.
(* Goal: divide a (Z.sub b c) *)
apply divide_intro with (q - q').
(* Goal: @eq Z (Z.sub b c) (Z.mul (Z.sub q q') a) *)
rewrite Hq; rewrite Hq'; ring.
Qed.

Lemma divide_left : forall a b c : Z, (a | b) -> (a | b * c).
Proof.
(* Goal: forall (a b c : Z) (_ : divide a b), divide a (Z.mul b c) *)
simple induction 1; intros q Hq; apply divide_intro with (q * c).
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite Hq; ring.
Qed.

Lemma divide_right : forall a b c : Z, (a | c) -> (a | b * c).
Proof.
(* Goal: forall (a b c : Z) (_ : divide a c), divide a (Z.mul b c) *)
simple induction 1; intros q Hq; apply divide_intro with (q * b).
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite Hq; ring.
Qed.

Lemma divide_a_ab : forall a b : Z, (a | a * b).
Proof.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
intros; apply divide_intro with b; ring.
Qed.

Lemma divide_a_ba : forall a b : Z, (a | b * a).
Proof.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
intros; apply divide_intro with b; ring.
Qed.

Hint Resolve divide_plus divide_opp divide_opp_rev divide_opp_left
  divide_opp_left_rev divide_minus divide_left divide_right divide_a_ab
  divide_a_ba.


(** Trivial lemmas to do case analysis over [x:Z]. *)

Lemma z_case_0_1 :
 forall x : Z, x <= -2 \/ x = -1 \/ x = 0 \/ x = 1 \/ x >= 2.
Proof. intro; omega. Qed.

Lemma z_case_0 : forall x : Z, x <= -1 \/ x = 0 \/ x >= 1.
Proof. intro; omega. Qed.


(** Only [1] and [-1] divide [1]. *)

Lemma divide_1 : forall x : Z, (x | 1) -> x = 1 \/ x = -1.
Proof.
(* Goal: forall (a b : Z) (_ : divide a b) (_ : not (@eq Z b Z0)), Z.le (Z.abs a) (Z.abs b) *)
simple induction 1; intros.
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
elim (z_case_0_1 x); intuition; elim (z_case_0 q); intuition.
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
assert (q * x >= 1 * 2). 
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
replace (q * x) with (- q * - x); try ring.
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H3 in H0; omega.
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
assert (- (q * x) >= 1 * 2). 
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
replace (- (q * x)) with (q * - x); try ring.
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H1 in H0; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H1 in H0; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H1 in H0; omega.
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
assert (- (q * x) >= 1 * 2). 
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
replace (- (q * x)) with (- q * x); try ring.
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H3 in H0; omega.
(* Goal: or (@eq Z x (Zpos xH)) (@eq Z x (Zneg xH)) *)
assert (q * x >= 1 * 2). 
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
omega.
Qed.


(** If [a] divides [b] and [b] divides [a] 
    then [a] is [b] or [-b]. *)

Lemma divide_antisym : forall a b : Z, (a | b) -> (b | a) -> a = b \/ a = - b.
Proof.
(* Goal: forall (a b : Z) (_ : divide a b) (_ : not (@eq Z b Z0)), Z.le (Z.abs a) (Z.abs b) *)
simple induction 1; intros.
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
inversion H1.
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
rewrite H0 in H2; clear H H1.
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
case (Z_zerop a); intro.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
left; rewrite H0; rewrite e; ring.
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
assert (Hqq0 : q0 * q = 1).
(* Goal: @eq Z (Z.mul q0 q) (Zpos xH) *)
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
apply Zmult_reg_l with a.
(* Goal: not (@eq Z a Z0) *)
(* Goal: @eq Z (Z.mul a (Z.mul q0 q)) (Z.mul a (Zpos xH)) *)
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
assumption.
(* Goal: @eq Z (Z.mul a (Z.mul q0 q)) (Z.mul a (Zpos xH)) *)
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
ring_simplify.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
pattern a at 2 in |- *; rewrite H2; ring.
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
assert (q | 1).
(* Goal: divide q (Zpos xH) *)
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
rewrite <- Hqq0; auto.
(* Goal: or (@eq Z a b) (@eq Z a (Z.opp b)) *)
elim (divide_1 q H); intros.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H1 in H0; left; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H1 in H0; right; omega.
Qed.


(** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)

Lemma Zabs_ind :
 forall (P : Z -> Prop) (x : Z),
 (x >= 0 -> P x) -> (x <= 0 -> P (- x)) -> P (Zabs x).
Proof.
(* Goal: forall (P : forall _ : Z, Prop) (x : Z) (_ : forall _ : Z.ge x Z0, P x) (_ : forall _ : Z.le x Z0, P (Z.opp x)), P (Z.abs x) *)
intros; elim (Z_lt_ge_dec x 0); intro. 
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite Zabs_non_eq. apply H0; omega. omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite Zabs_eq. apply H; assumption. omega.
Qed.

Lemma divide_bounds : forall a b : Z, (a | b) -> b <> 0 -> Zabs a <= Zabs b.
Proof.
(* Goal: forall (a b : Z) (_ : divide a b) (_ : not (@eq Z b Z0)), Z.le (Z.abs a) (Z.abs b) *)
simple induction 1; intros.
pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs b) in |- *;
 apply Zabs_ind; intros.
(* a >= 0, b >= 0 *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim (z_case_0 q); intro.
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
assert (- b >= 1 * 0).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) Z0) *)
(* Goal: Z.le a b *)
(* Goal: Z.le a b *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
replace (- b) with (- q * a).
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Z.opp q) a) (Z.opp b) *)
(* Goal: Z.le a b *)
(* Goal: Z.le a b *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H0; ring. omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim H4; intro; clear H4. 
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H5 in H0; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
apply Zge_le.
(* Goal: Z.ge (Z.opp b) a *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
replace a with (1 * a).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
ring.
(* a >= 0, b <= 0 *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim (z_case_0 q); intro.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
apply Zge_le.
(* Goal: Z.ge (Z.opp b) a *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
replace a with (1 * a).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.opp (Z.mul q a)) (Z.mul (Zpos xH) a) *)
(* Goal: @eq Z (Z.mul (Zpos xH) a) a *)
(* Goal: Z.le a (Z.opp b) *)
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
replace (- (q * a)) with (- q * a).
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
ring. ring.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim H4; intro; clear H4. 
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H5 in H0; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
assert (b >= 1 * 0).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
omega.
(* a <= 0, b >= 0 *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim (z_case_0 q); intro.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
apply Zge_le.
(* Goal: Z.ge (Z.opp b) (Z.opp a) *)
replace (- a) with (1 * - a).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.mul q a) (Z.mul (Zpos xH) Z0) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
replace (q * a) with (- q * - a).
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
ring. ring.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim H4; intro; clear H4. 
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H5 in H0; omega.
(* Goal: Z.le (Z.opp a) b *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
assert (- b >= 1 * 0).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.opp (Z.mul q a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
replace (- (q * a)) with (q * - a).
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
ring. omega.
(* a <= 0, b <= 0 *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim (z_case_0 q); intro.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
assert (b >= 1 * 0).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.mul q a) (Z.mul (Zpos xH) Z0) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
replace (q * a) with (- q * - a).
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
ring. omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
elim H4; intro; clear H4. 
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
rewrite H5 in H0; omega.
(* Goal: Z.le (Z.opp a) (Z.opp b) *)
apply Zge_le.
(* Goal: Z.ge (Z.opp b) (Z.opp a) *)
replace (- a) with (1 * - a).
(* Goal: Z.ge (Z.opp b) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
rewrite H0.
(* Goal: Z.ge (Z.opp (Z.mul q a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
replace (- (q * a)) with (q * - a).
(* Goal: Z.ge (Z.mul q (Z.opp a)) (Z.mul (Zpos xH) (Z.opp a)) *)
(* Goal: @eq Z (Z.mul q (Z.opp a)) (Z.opp (Z.mul q a)) *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
apply Zmult_ge_compat; omega.
(* Goal: @eq Z (Z.mul (Zpos xH) (Z.opp a)) (Z.opp a) *)
ring. ring.
Qed.
