Qreduction.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Normalisation functions for rational numbers.

Require Export QArith_base.
Require Import Znumtheory.

Notation Z2P := Z.to_pos (only parsing).
Notation Z2P_correct := Z2Pos.id (only parsing).

Simplification of fractions using Z.gcd. This version can compute within Coq.

Definition Qred (q:Q) :=
  let (q1,q2) := q in
  let (r1,r2) := snd (Z.ggcd q1 (Zpos q2))
  in r1#(Z.to_pos r2).

Lemma Qred_correct : forall q, (Qred q) == q.forall q : Q, Qred q == q
Proof.forall q : Q, Qred q == q
  unfold Qred, Qeq; intros (n,d); simpl.n:Z
d:positive
Qnum
  (let (r1, r2) := snd (Z.ggcd n (Z.pos d)) in
   r1 # Z.to_pos r2) * Z.pos d =
n *
QDen
  (let (r1, r2) := snd (Z.ggcd n (Z.pos d)) in
   r1 # Z.to_pos r2)
  generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d))
    (Z.ggcd_correct_divisors n (Zpos d)).n:Z
d:positive
fst (Z.ggcd n (Z.pos d)) = Z.gcd n (Z.pos d) ->
0 <= Z.gcd n (Z.pos d) ->
(let
 '(g, (aa, bb)) := Z.ggcd n (Z.pos d) in
  n = g * aa /\ Z.pos d = g * bb) ->
Qnum
  (let (r1, r2) := snd (Z.ggcd n (Z.pos d)) in
   r1 # Z.to_pos r2) * Z.pos d =
n *
QDen
  (let (r1, r2) := snd (Z.ggcd n (Z.pos d)) in
   r1 # Z.to_pos r2)
  destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl.n:Z
d:positive
g, nn, dd:Z
g = Z.gcd n (Z.pos d) ->
0 <= Z.gcd n (Z.pos d) ->
n = g * nn /\ Z.pos d = g * dd ->
nn * Z.pos d = n * Z.pos (Z.to_pos dd)
  Open Scope Z_scope.n:Z
d:positive
g, nn, dd:Z
g = Z.gcd n (Z.pos d) ->
0 <= Z.gcd n (Z.pos d) ->
n = g * nn /\ Z.pos d = g * dd ->
nn * Z.pos d = n * Z.pos (Z.to_pos dd)
  intros Hg LE (Hn,Hd).n:Z
d:positive
g, nn, dd:Z
Hg:g = Z.gcd n (Z.pos d)
LE:0 <= Z.gcd n (Z.pos d)
Hn:n = g * nn
Hd:Z.pos d = g * dd
nn * Z.pos d = n * Z.pos (Z.to_pos dd) rewrite Hd, Hn.n:Z
d:positive
g, nn, dd:Z
Hg:g = Z.gcd n (Z.pos d)
LE:0 <= Z.gcd n (Z.pos d)
Hn:n = g * nn
Hd:Z.pos d = g * dd
nn * (g * dd) = g * nn * Z.pos (Z.to_pos dd)
  rewrite <- Hg in LE; clear Hg.n:Z
d:positive
g, nn, dd:Z
LE:0 <= g
Hn:n = g * nn
Hd:Z.pos d = g * dd
nn * (g * dd) = g * nn * Z.pos (Z.to_pos dd)
  assert (0 <> g) by (intro; subst; discriminate).n:Z
d:positive
g, nn, dd:Z
LE:0 <= g
Hn:n = g * nn
Hd:Z.pos d = g * dd
H:0 <> g
nn * (g * dd) = g * nn * Z.pos (Z.to_pos dd)
  rewrite Z2Pos.id.n:Z
d:positive
g, nn, dd:Z
LE:0 <= g
Hn:n = g * nn
Hd:Z.pos d = g * dd
H:0 <> g
nn * (g * dd) = g * nn * dd
n:Z
d:positive
g, nn, dd:Z
LE:0 <= g
Hn:n = g * nn
Hd:Z.pos d = g * dd
H:0 <> g
0 < dd ring.n:Z
d:positive
g, nn, dd:Z
LE:0 <= g
Hn:n = g * nn
Hd:Z.pos d = g * dd
H:0 <> g
0 < dd
  rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega].
  Close Scope Z_scope.
Qed.

Lemma Qred_complete : forall p q,  p==q -> Qred p = Qred q.forall p q : Q, p == q -> Qred p = Qred q
Proof.forall p q : Q, p == q -> Qred p = Qred q
  intros (a,b) (c,d).a:Z
b:positive
c:Z
d:positive
a # b == c # d -> Qred (a # b) = Qred (c # d)
  unfold Qred, Qeq in *; simpl in *.a:Z
b:positive
c:Z
d:positive
(a * Z.pos d)%Z = (c * Z.pos b)%Z ->
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  Open Scope Z_scope.a:Z
b:positive
c:Z
d:positive
a * Z.pos d = c * Z.pos b ->
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  intros H.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b))
    (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
fst (Z.ggcd a (Z.pos b)) = Z.gcd a (Z.pos b) ->
Zis_gcd a (Z.pos b) (Z.gcd a (Z.pos b)) ->
0 <= Z.gcd a (Z.pos b) ->
(let
 '(g, (aa, bb)) := Z.ggcd a (Z.pos b) in
  a = g * aa /\ Z.pos b = g * bb) ->
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
fst (g, (aa, bb)) = Z.gcd a (Z.pos b) ->
Zis_gcd a (Z.pos b) (Z.gcd a (Z.pos b)) ->
0 <= Z.gcd a (Z.pos b) ->
a = g * aa /\ Z.pos b = g * bb ->
(let (r1, r2) := snd (g, (aa, bb)) in r1 # Z.to_pos r2) =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  simpl.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
g = Z.gcd a (Z.pos b) ->
Zis_gcd a (Z.pos b) (Z.gcd a (Z.pos b)) ->
0 <= Z.gcd a (Z.pos b) ->
a = g * aa /\ Z.pos b = g * bb ->
aa # Z.to_pos bb =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2) intros <- Hg1 Hg2 (Hg3,Hg4).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
aa # Z.to_pos bb =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  assert (Hg0 : g <> 0) by (intro; now subst g).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
aa # Z.to_pos bb =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d))
    (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
fst (Z.ggcd c (Z.pos d)) = Z.gcd c (Z.pos d) ->
Zis_gcd c (Z.pos d) (Z.gcd c (Z.pos d)) ->
0 <= Z.gcd c (Z.pos d) ->
(let
 '(g0, (aa0, bb0)) := Z.ggcd c (Z.pos d) in
  c = g0 * aa0 /\ Z.pos d = g0 * bb0) ->
aa # Z.to_pos bb =
(let (r1, r2) := snd (Z.ggcd c (Z.pos d)) in
 r1 # Z.to_pos r2)
  destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
fst (g', (cc, dd)) = Z.gcd c (Z.pos d) ->
Zis_gcd c (Z.pos d) (Z.gcd c (Z.pos d)) ->
0 <= Z.gcd c (Z.pos d) ->
c = g' * cc /\ Z.pos d = g' * dd ->
aa # Z.to_pos bb =
(let (r1, r2) := snd (g', (cc, dd)) in
 r1 # Z.to_pos r2)
  simpl.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
g' = Z.gcd c (Z.pos d) ->
Zis_gcd c (Z.pos d) (Z.gcd c (Z.pos d)) ->
0 <= Z.gcd c (Z.pos d) ->
c = g' * cc /\ Z.pos d = g' * dd ->
aa # Z.to_pos bb = cc # Z.to_pos dd intros <- Hg'1 Hg'2 (Hg'3,Hg'4).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
aa # Z.to_pos bb = cc # Z.to_pos dd
  assert (Hg'0 : g' <> 0) by (intro; now subst g').a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
aa # Z.to_pos bb = cc # Z.to_pos dd

  elim (rel_prime_cross_prod aa bb cc dd).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
aa = cc ->
bb = dd -> aa # Z.to_pos bb = cc # Z.to_pos dd
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
rel_prime aa bb
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
rel_prime cc dd
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
bb > 0
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
dd > 0
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
aa * dd = bb * cc
  -a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
aa = cc ->
bb = dd -> aa # Z.to_pos bb = cc # Z.to_pos dd congruence.
  - (*rel_prime*)a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
rel_prime aa bb
    constructor.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | aa)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | bb)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
forall x : Z, (x | aa) -> (x | bb) -> (x | 1)
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | aa) exists aa; auto with zarith.
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | bb) exists bb; auto with zarith.
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
forall x : Z, (x | aa) -> (x | bb) -> (x | 1) intros x Ha Hb.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(x | 1)
      destruct Hg1 as (Hg11,Hg12,Hg13).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(x | 1)
      destruct (Hg13 (g*x)) as (x',Hx).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | a)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | Z.pos b)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
x':Z
Hx:g = x' * (g * x)
(x | 1)
      {a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | a) rewrite Hg3.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | g * aa)
        destruct Ha as (xa,Hxa); exists xa; rewrite Hxa; ring. }a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | Z.pos b)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
x':Z
Hx:g = x' * (g * x)
(x | 1)
      {a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | Z.pos b) rewrite Hg4.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
(g * x | g * bb)
        destruct Hb as (xb,Hxb); exists xb; rewrite Hxb; ring. }a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
x':Z
Hx:g = x' * (g * x)
(x | 1)
      exists x'.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
x':Z
Hx:g = x' * (g * x)
1 = x' * x
      apply Z.mul_reg_l with g; auto.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg11:(g | a)
Hg12:(g | Z.pos b)
Hg13:forall x0 : Z,
(x0 | a) -> (x0 | Z.pos b) -> (x0 | g)
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Ha:(x | aa)
Hb:(x | bb)
x':Z
Hx:g = x' * (g * x)
g * 1 = g * (x' * x) rewrite Hx at 1; ring.
  - (* rel_prime *)a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
rel_prime cc dd
    constructor.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | cc)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | dd)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
forall x : Z, (x | cc) -> (x | dd) -> (x | 1)
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | cc) exists cc; auto with zarith.
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
(1 | dd) exists dd; auto with zarith.
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
forall x : Z, (x | cc) -> (x | dd) -> (x | 1) intros x Hc Hd.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
(x | 1)
      inversion Hg'1 as (Hg'11,Hg'12,Hg'13).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(x | 1)
      destruct (Hg'13 (g'*x)) as (x',Hx).a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | c)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | Z.pos d)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
x':Z
Hx:g' = x' * (g' * x)
(x | 1)
      {a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | c) rewrite Hg'3.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | g' * cc)
        destruct Hc as (xc,Hxc); exists xc; rewrite Hxc; ring. }a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | Z.pos d)
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
x':Z
Hx:g' = x' * (g' * x)
(x | 1)
      {a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | Z.pos d) rewrite Hg'4.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
(g' * x | g' * dd)
        destruct Hd as (xd,Hxd); exists xd; rewrite Hxd; ring. }a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
x':Z
Hx:g' = x' * (g' * x)
(x | 1)
      exists x'.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
x':Z
Hx:g' = x' * (g' * x)
1 = x' * x
      apply Z.mul_reg_l with g'; auto.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
x:Z
Hc:(x | cc)
Hd:(x | dd)
Hg'11:(g' | c)
Hg'12:(g' | Z.pos d)
Hg'13:forall x0 : Z,
(x0 | c) -> (x0 | Z.pos d) -> (x0 | g')
x':Z
Hx:g' = x' * (g' * x)
g' * 1 = g' * (x' * x) rewrite Hx at 1; ring.
  -a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
bb > 0 apply Z.lt_gt.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
0 < bb
    rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hg4 | omega].
  -a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
dd > 0 apply Z.lt_gt.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
0 < dd
    rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | omega].
  -a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
aa * dd = bb * cc apply Z.mul_reg_l with (g*g').a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
g * g' <> 0
a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
g * g' * (aa * dd) = g * g' * (bb * cc)
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
g * g' <> 0 rewrite Z.mul_eq_0.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
~ (g = 0 \/ g' = 0) now destruct 1.
    *a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
g * g' * (aa * dd) = g * g' * (bb * cc) rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4.a:Z
b:positive
c:Z
d:positive
H:a * Z.pos d = c * Z.pos b
g, aa, bb:Z
Hg1:Zis_gcd a (Z.pos b) g
Hg2:0 <= g
Hg3:a = g * aa
Hg4:Z.pos b = g * bb
Hg0:g <> 0
g', cc, dd:Z
Hg'1:Zis_gcd c (Z.pos d) g'
Hg'2:0 <= g'
Hg'3:c = g' * cc
Hg'4:Z.pos d = g' * dd
Hg'0:g' <> 0
a * Z.pos d = g * g' * (bb * cc)
      now rewrite Z.mul_shuffle1, <- Hg'3, <- Hg4, H, Z.mul_comm.
  Close Scope Z_scope.
Qed.

Lemma Qred_eq_iff q q' : Qred q = Qred q' <-> q == q'.q, q':Q
Qred q = Qred q' <-> q == q'
Proof.q, q':Q
Qred q = Qred q' <-> q == q'
 split.q, q':Q
Qred q = Qred q' -> q == q'
q, q':Q
q == q' -> Qred q = Qred q'
 -q, q':Q
Qred q = Qred q' -> q == q' intros E.q, q':Q
E:Qred q = Qred q'
q == q' rewrite <- (Qred_correct q), <- (Qred_correct q').q, q':Q
E:Qred q = Qred q'
Qred q == Qred q'
   now rewrite E.
 -q, q':Q
q == q' -> Qred q = Qred q' apply Qred_complete.
Qed.

Add Morphism Qred with signature (Qeq ==> Qeq) as Qred_comp.forall x y : Q, x == y -> Qred x == Qred y
Proof.forall x y : Q, x == y -> Qred x == Qred y
  intros.x, y:Q
H:x == y
Qred x == Qred y now rewrite !Qred_correct.
Qed.

Definition Qplus' (p q : Q) := Qred (Qplus p q).
Definition Qmult' (p q : Q) := Qred (Qmult p q).
Definition Qminus' x y := Qred (Qminus x y).

Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).forall p q : Q, Qplus' p q == p + q
Proof.forall p q : Q, Qplus' p q == p + q
  intros; unfold Qplus'; apply Qred_correct; auto.
Qed.

Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q).forall p q : Q, Qmult' p q == p * q
Proof.forall p q : Q, Qmult' p q == p * q
  intros; unfold Qmult'; apply Qred_correct; auto.
Qed.

Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).forall p q : Q, Qminus' p q == p - q
Proof.forall p q : Q, Qminus' p q == p - q
  intros; unfold Qminus'; apply Qred_correct; auto.
Qed.

Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp.forall x y : Q,
x == y ->
forall x0 y0 : Q,
x0 == y0 -> Qplus' x x0 == Qplus' y y0
Proof.forall x y : Q,
x == y ->
forall x0 y0 : Q,
x0 == y0 -> Qplus' x x0 == Qplus' y y0
  intros; unfold Qplus'.x, y:Q
H:x == y
x0, y0:Q
H0:x0 == y0
Qred (x + x0) == Qred (y + y0)
  rewrite H, H0; auto with qarith.
Qed.

Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp.forall x y : Q,
x == y ->
forall x0 y0 : Q,
x0 == y0 -> Qmult' x x0 == Qmult' y y0
Proof.forall x y : Q,
x == y ->
forall x0 y0 : Q,
x0 == y0 -> Qmult' x x0 == Qmult' y y0
  intros; unfold Qmult'.x, y:Q
H:x == y
x0, y0:Q
H0:x0 == y0
Qred (x * x0) == Qred (y * y0)
  rewrite H, H0; auto with qarith.
Qed.

Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp.forall x y : Q,
x == y ->
forall x0 y0 : Q,
x0 == y0 -> Qminus' x x0 == Qminus' y y0
Proof.forall x y : Q,
x == y ->
forall x0 y0 : Q,
x0 == y0 -> Qminus' x x0 == Qminus' y y0
  intros; unfold Qminus'.x, y:Q
H:x == y
x0, y0:Q
H0:x0 == y0
Qred (x - x0) == Qred (y - y0)
  rewrite H, H0; auto with qarith.
Qed.

Lemma Qred_opp: forall q, Qred (-q) = - (Qred q).forall q : Q, Qred (- q) = - Qred q
Proof.forall q : Q, Qred (- q) = - Qred q
  intros (x, y); unfold Qred; simpl.x:Z
y:positive
(let (r1, r2) := snd (Z.ggcd (- x) (Z.pos y)) in
 r1 # Z.to_pos r2) =
-
(let (r1, r2) := snd (Z.ggcd x (Z.pos y)) in
 r1 # Z.to_pos r2)
  rewrite Z.ggcd_opp; case Z.ggcd; intros p1 (p2, p3); simpl.x:Z
y:positive
p1, p2, p3:Z
- p2 # Z.to_pos p3 = - (p2 # Z.to_pos p3)
  unfold Qopp; auto.
Qed.

Theorem Qred_compare: forall x y,
  Qcompare x y = Qcompare (Qred x) (Qred y).forall x y : Q, (x ?= y) = (Qred x ?= Qred y)
Proof.forall x y : Q, (x ?= y) = (Qred x ?= Qred y)
  intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
Qed.

Lemma Qred_le q q' : Qred q <= Qred q' <-> q <= q'.q, q':Q
Qred q <= Qred q' <-> q <= q'
Proof.q, q':Q
Qred q <= Qred q' <-> q <= q'
  now rewrite !Qle_alt, <- Qred_compare.
Qed.

Lemma Qred_lt q q' : Qred q < Qred q' <-> q < q'.q, q':Q
Qred q < Qred q' <-> q < q'
Proof.q, q':Q
Qred q < Qred q' <-> q < q'
  now rewrite !Qlt_alt, <- Qred_compare.
Qed.