(* Copyright (C) 2005-2008 Sebastien Briais *)
(* http://lamp.epfl.ch/~sbriais/ *)

(* This library 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 library 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 *)
(* Lesser General Public License for more details. *)

(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)

Require Import missing.
Require Import division.
Require Import euclide.
Require Import power.
Require Import Wf_nat.

Unset Standard Proposition Elimination Names.

(** d is a common divisor of a and b if d | a and d | b *)
Definition is_cd (d a b : nat) := (divides a d)/\(divides b d).

(** d is a greatest common divisor of a and b if it is a maximal common divisor *)
Definition is_gcd (d a b:nat) := (is_cd d a b)/\(forall (d':nat),(is_cd d' a b)->(divides d d')).

(** there is at most one gcd of a and b *)
Theorem gcd_unique : forall (d d' a b:nat),(is_gcd d a b)->(is_gcd d' a b)->d=d'.
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H;elim H0;intros.
(* Goal: @eq nat d d' *)
  apply divides_antisym;auto.
Qed.

(** gcd(a,b) = gcd(b,a) *)
Lemma gcd_sym : forall (d a b:nat),(is_gcd d a b)->(is_gcd d b a).
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H;intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: is_cd d b a *)
(* Goal: forall (d' : nat) (_ : is_cd d' b a), divides d d' *)
  red;red in H0;tauto.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: divides d d' *)
  apply H1.
(* Goal: is_cd d' a b *)
  red;red in H2;tauto.
Qed.

(** gcd(0,a)=a *)
Lemma gcd_zero : forall (a:nat),(is_gcd a O a).
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: not (@eq nat d O) *)
  intro.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: is_cd a O a *)
(* Goal: forall (d' : nat) (_ : is_cd d' O a), divides a d' *)
  red;split;[apply zero_max_div | apply divides_refl].
(* Goal: forall (d' : nat) (_ : is_cd d' (S O) a), divides (S O) d' *)
  unfold is_cd;tauto.
Qed.

(** gcd(1,a)=1 *)
Lemma gcd_one : forall (a:nat),(is_gcd 1 1 a).
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: is_cd (S O) (S O) a *)
(* Goal: forall (d' : nat) (_ : is_cd d' (S O) a), divides (S O) d' *)
  red;split;[apply divides_refl | apply one_min_div].
(* Goal: forall (d' : nat) (_ : is_cd d' (S O) a), divides (S O) d' *)
  unfold is_cd;tauto.
Qed.

(** if a <= b then gcd(a,b)=gcd(a,b-a) *)
Lemma gcd_minus : forall (d a b:nat),(a <= b)->((is_gcd d a b)<->(is_gcd d a (b-a))).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: not (@eq nat d O) *)
  split;intro.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H0;intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: is_cd d a (Init.Nat.sub b a) *)
(* Goal: forall (d' : nat) (_ : is_cd d' a (Init.Nat.sub b a)), divides d d' *)
(* Goal: and (is_cd d a b) (forall (d' : nat) (_ : is_cd d' a b), divides d d') *)
  red in H1;red.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H1;intros.
(* Goal: and (divides b d') (divides (remainder_euclide a b H) d') *)
  split;try tauto.
(* Goal: divides (Init.Nat.sub b a) d *)
(* Goal: forall (d' : nat) (_ : is_cd d' a (Init.Nat.sub b a)), divides d d' *)
(* Goal: and (is_cd d a b) (forall (d' : nat) (_ : is_cd d' a b), divides d d') *)
  apply divides_minus;trivial.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  unfold is_cd;intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  apply H2;red;elim H3;intros.
(* Goal: and (divides a d') (divides b d') *)
(* Goal: and (is_cd d a b) (forall (d' : nat) (_ : is_cd d' a b), divides d d') *)
  split;[tauto | rewrite (le_plus_minus a b H);apply divides_plus;trivial].
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H0;unfold is_cd;intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: and (divides a d) (divides b d) *)
(* Goal: forall (d' : nat) (_ : and (divides a d') (divides b d')), divides d d' *)
  split;[tauto | elim H1;intros;rewrite (le_plus_minus a b H);apply divides_plus;trivial].
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: divides d d' *)
  elim H3;intros;apply H2.
(* Goal: and (divides a d') (divides (Init.Nat.sub b a) d') *)
  split;try (apply divides_minus);trivial.
Qed.

(** gcd(a,a) = a *)
Lemma gcd_refl : forall (a:nat),(is_gcd a a a).
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: and (is_cd a a a) (forall (d' : nat) (_ : is_cd d' a a), divides a d') *)
  unfold is_cd.
(* Goal: and (divides b d') (divides (remainder_euclide a b H) d') *)
  split;try tauto.
(* Goal: and (divides a a) (divides a a) *)
  split;apply divides_refl.
Qed.

(** two trivial lemmas: gcd(a,b) | a *)
Lemma gcd_div_l : forall (d a b:nat),(is_gcd d a b)->(divides a d).
(* Goal: forall (d a b : nat) (_ : is_gcd d a b), divides b d *)
  unfold is_gcd;unfold is_cd;intros;tauto.
Qed.

(** gcd(a,b) | b *)
Lemma gcd_div_r : forall (d a b:nat),(is_gcd d a b)->(divides b d).
(* Goal: forall (d a b : nat) (_ : is_gcd d a b), divides b d *)
  unfold is_gcd;unfold is_cd;intros;tauto.
Qed.

(** we now show that gcd(a,b) exists for all a and b (we even have an algorithm) *)
Definition f (x:nat*nat) := (fst x)+(snd x).

Definition R (x y:nat*nat) := (f x)<(f y).

Lemma Rwf : well_founded R.
(* Goal: @well_founded (prod nat nat) R *)
  unfold R.
(* Goal: @well_founded (prod nat nat) (fun x y : prod nat nat => lt (f x) (f y)) *)
  apply (well_founded_ltof (nat*nat) f).
Qed.

(** proof of existence of gcd(a,b): it relies on the relation gcd(a,b)=gcd(a,b-a) if a<=b *)
Lemma gcd_exists_prod : forall (x:nat*nat),{d:nat | (is_gcd d (fst x) (snd x))}.
(* Goal: forall x : prod nat nat, @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  apply (induction_ltof2 (nat*nat) f (fun x:nat*nat => {d:nat | (is_gcd d (fst x) (snd x))})).
(* Goal: forall (x : prod nat nat) (_ : forall (y : prod nat nat) (_ : ltof (prod nat nat) f y x), sum (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y)) (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y))) (@fst nat nat y) (@snd nat nat y))) (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y)) (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y))) (@fst nat nat y) (@snd nat nat y)))), sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  unfold ltof.
(* Goal: forall (x : prod nat nat) (_ : forall (y : prod nat nat) (_ : lt (f y) (f x)), sum (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y)) (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y))) (@fst nat nat y) (@snd nat nat y))) (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y)) (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y))) (@fst nat nat y) (@snd nat nat y)))), sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  unfold f.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  case (lt_eq_lt_dec (fst x) (snd x));intro.
(* Goal: not (@eq nat d O) *)
  case s;intro.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  destruct (fst x).
(* Goal: @sig nat (fun d : nat => is_gcd d O (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (S n) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  exists (snd x);apply gcd_zero.
(* Goal: @sig nat (fun d : nat => is_gcd d (S n) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  elim (H (S n,snd x-S n)).
(* Goal: not (@eq nat d O) *)
  simpl;intro d;intro.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: lt (Init.Nat.add (@snd nat nat x) (remainder_euclide (@fst nat nat x) (@snd nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
  exists d.
(* Goal: is_gcd d (S n) (@snd nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@snd nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@snd nat nat x) (S n))))) (Init.Nat.add (S n) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  elim (gcd_minus d (S n) (snd x));try (auto with arith).
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl.
(* Goal: lt (S (Init.Nat.add n (Init.Nat.sub (@fst nat nat x) (S n)))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  omega.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  rewrite e;exists (snd x);apply gcd_refl.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  destruct (snd x).
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) O) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (S n)) *)
  exists (fst x);apply gcd_sym;apply gcd_zero.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (S n)) *)
  elim (H (S n,fst x-S n)).
(* Goal: not (@eq nat d O) *)
  simpl;intro d;intro.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: lt (Init.Nat.add (@snd nat nat x) (remainder_euclide (@fst nat nat x) (@snd nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
  exists d.
(* Goal: is_gcd d (@fst nat nat x) (@snd nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat x) (remainder_euclide (@snd nat nat x) (@fst nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  apply gcd_sym.
(* Goal: is_gcd d (S n) (@fst nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  elim (gcd_minus d (S n) (fst x));try (auto with arith).
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl.
(* Goal: lt (S (Init.Nat.add n (Init.Nat.sub (@fst nat nat x) (S n)))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  omega.
Qed.

(** here we are: the gcd exists *)
Theorem gcd_exists : forall (a b:nat),{d:nat | (is_gcd d a b)}.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: @sig nat (fun d : nat => is_gcd d a b) *)
  elim (gcd_exists_prod (a,b)).
(* Goal: forall (x : nat) (_ : is_gcd x (@fst nat nat (@pair nat nat a b)) (@snd nat nat (@pair nat nat a b))), @sig nat (fun d : nat => is_gcd d a b) *)
  simpl;intro d;intro;exists d;trivial.
Qed.

(** take the first projection of the proof *)
Definition gcd (a b:nat) := let (d,_):=(gcd_exists a b) in d.

(** the gcd is the gcd! *)
Lemma gcd_is_gcd : forall (a b:nat),(is_gcd (gcd a b) a b).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: is_gcd (gcd a b) a b *)
  unfold gcd.
(* Goal: is_gcd (let (d, _) := gcd_exists a b in d) a b *)
  generalize (gcd_exists a b).
(* Goal: forall s : @sig nat (fun d : nat => is_gcd d a b), is_gcd (let (d, _) := s in d) a b *)
  intro;elim s;intro d;trivial.
Qed.

(** a and b are relatively prime if gcd(a,b)=1 *)
Definition rel_prime (a b:nat) := (is_gcd 1 a b). 

(** if a and b are relatively prime then so are b and a *)
Lemma rel_prime_sym : forall (a b:nat),(rel_prime a b)->(rel_prime b a).
(* Goal: sumbool (rel_prime a b) (not (rel_prime a b)) *)
  unfold rel_prime.
(* Goal: forall (a b : nat) (_ : is_gcd (S O) a b), is_gcd (S O) b a *)
  intros;apply gcd_sym;trivial.
Qed.

(** for all a, a and 1 are relatively prime *)
Lemma rel_prime_1 : forall (a:nat),(rel_prime a 1).
(* Goal: sumbool (rel_prime a b) (not (rel_prime a b)) *)
  unfold rel_prime.
(* Goal: forall a : nat, is_gcd (S O) a (S O) *)
  intros;apply gcd_sym;apply gcd_one.
Qed.

(** we have that a/gcd(a,b) and b/gcd(a,b) are relatively prime *)
Lemma gcd_rel_prime : forall (d a b:nat)(H:(is_gcd d a b)),(d <> O)->(rel_prime (quo a d (gcd_div_l d a b H)) (quo b d (gcd_div_r d a b H))).
(* Goal: sumbool (rel_prime a b) (not (rel_prime a b)) *)
  unfold rel_prime.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  generalize (quo_is_quo a d (gcd_div_l d a b H));intro.
(* Goal: not (@eq nat d O) *)
  generalize (quo_is_quo b d (gcd_div_r d a b H));intro.
(* Goal: and (is_cd a a a) (forall (d' : nat) (_ : is_cd d' a a), divides a d') *)
  unfold is_gcd;split;unfold is_cd.
(* Goal: and (divides a (S O)) (divides b (S O)) *)
(* Goal: forall (d' : nat) (_ : and (divides a d') (divides b d')), divides (S O) d' *)
  split;apply one_min_div.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H3;intros.
(* Goal: not (@eq nat d O) *)
  elim H4;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H5;intro q';intro.
(* Goal: divides (S O) d' *)
  rewrite H6 in H1.
(* Goal: divides (S O) d' *)
  rewrite H7 in H2.
(* Goal: divides (S O) d' *)
  assert (divides d (d*d')).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  red in H;elim H;intros.
(* Goal: divides d (Init.Nat.mul d d') *)
(* Goal: divides (S O) d' *)
  apply H9;red;split;[exists q;rewrite H1;ring | exists q';rewrite H2;ring].
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H8;intros.
(* Goal: divides (S O) d' *)
  exists x.
(* Goal: @eq nat (S O) (Init.Nat.mul d' x) *)
  apply mult_lemma6 with d;trivial.
(* Goal: @eq nat (Init.Nat.mul d (S O)) (Init.Nat.mul d (Init.Nat.mul d' x)) *)
  rewrite mult_assoc;rewrite <- H9;auto with arith.
Qed.

(** if q<>0 then gcd(p,q)<>0 *)
Lemma gcd_non_zero : forall (d p q:nat),(q<>O)->(is_gcd d p q)->(d<>O).
(* Goal: forall (d p q : nat) (_ : not (@eq nat q O)) (_ : is_gcd d p q), not (@eq nat d O) *)
  unfold is_gcd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H0;intros.
(* Goal: not (@eq nat d O) *)
  intro.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H1;intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H5;intros.
(* Goal: False *)
  rewrite H3 in H6;simpl in H6;auto.
Qed.

(** we now exhibit an algorithm that computes Bezout coefficient: for all a b, there is u and v such that a*u-b*v = gcd(a,b) or b*v-a*u = gcd(a,b) *)
(** the 4 lemmae gives the idea of the algorithm *)
Lemma bezout_aux1 : forall (x y u v:nat),(x<=y)->(is_gcd (u*x-v*(y-x)) x (y-x))->(is_gcd ((u+v)*x-v*y) x y).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim (gcd_minus ((u+v)*x-v*y) x y H);intros.
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul v y) (Init.Nat.mul (Init.Nat.add u v) x)) x y *)
  apply H2.
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul (Init.Nat.add u v) x) (Init.Nat.mul v y)) x (Init.Nat.sub y x) *)
  rewrite mult_plus_distr_r;rewrite <- minus_minus_lemma1;try (auto with arith);rewrite <- mult_minus_lemma2;trivial.
Qed.

Lemma bezout_aux2 : forall (x y u v:nat),(x<=y)->(is_gcd (v*(y-x)-u*x) x (y-x))->(is_gcd (v*y-(u+v)*x) x y).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim (gcd_minus (v*y-(u+v)*x) x y H);intros.
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul v y) (Init.Nat.mul (Init.Nat.add u v) x)) x y *)
  apply H2.
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul v y) (Init.Nat.mul (Init.Nat.add u v) x)) x (Init.Nat.sub y x) *)
  rewrite mult_plus_distr_r;rewrite plus_comm;rewrite <- minus_minus_lemma2;rewrite <- mult_minus_lemma2;trivial.
Qed.

(** Bezout coefficient *)
Lemma bezout_exists_prod : forall (x:nat*nat),{y:nat*nat | (is_gcd ((fst y)*(fst x)-(snd y)*(snd x)) (fst x) (snd x))}+{y:nat*nat | (is_gcd ((snd y)*(snd x)-(fst y)*(fst x)) (fst x) (snd x))}.
(* Goal: forall x : prod nat nat, sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  apply (induction_ltof2 (nat*nat) f (fun x:nat*nat => ({y:nat*nat | (is_gcd ((fst y)*(fst x)-(snd y)*(snd x)) (fst x) (snd x))}+{y:nat*nat | (is_gcd ((snd y)*(snd x)-(fst y)*(fst x)) (fst x) (snd x))})%type)).
(* Goal: forall (x : prod nat nat) (_ : forall (y : prod nat nat) (_ : ltof (prod nat nat) f y x), sum (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y)) (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y))) (@fst nat nat y) (@snd nat nat y))) (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y)) (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y))) (@fst nat nat y) (@snd nat nat y)))), sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  unfold ltof.
(* Goal: forall (x : prod nat nat) (_ : forall (y : prod nat nat) (_ : lt (f y) (f x)), sum (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y)) (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y))) (@fst nat nat y) (@snd nat nat y))) (@sig (prod nat nat) (fun y0 : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y0) (@snd nat nat y)) (Init.Nat.mul (@fst nat nat y0) (@fst nat nat y))) (@fst nat nat y) (@snd nat nat y)))), sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  unfold f.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  case (lt_eq_lt_dec (fst x) (snd x));intro.
(* Goal: not (@eq nat d O) *)
  case s;intro.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  destruct (fst x).
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) O) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) O (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) O)) O (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (S n)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (S n) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (S n))) (S n) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  right;exists (0,1);simpl;rewrite <- minus_n_O;rewrite plus_comm;simpl;apply gcd_zero.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (S n)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (S n) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (S n))) (S n) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  elim (H (S n,snd x-S n));try (intro;simpl).
(* Goal: not (@eq nat d O) *)
  elim a;intro y;intro.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (S n)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (S n) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (S n))) (S n) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (S n)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (S n) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (S n))) (S n) (@snd nat nat x))) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@snd nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@snd nat nat x) (S n))))) (Init.Nat.add (S n) (@snd nat nat x)) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  left;exists ((fst y)+(snd y),(snd y)).
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (S n)) (Init.Nat.mul (@fst nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (@fst nat nat x))) (S n) (@fst nat nat x) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (S n))) (@fst nat nat x) (S n))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (S n)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (S n))) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl;apply bezout_aux1;try (auto with arith).
(* Goal: not (@eq nat d O) *)
  elim b;intro y;intro.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (S n)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (S n) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (S n))) (S n) (@snd nat nat x))) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@snd nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@snd nat nat x) (S n))))) (Init.Nat.add (S n) (@snd nat nat x)) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  right;exists ((fst y)+(snd y),(snd y)).
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (S n))) (S n) (@fst nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl;apply bezout_aux2;try (auto with arith).
(* Goal: lt (S (Init.Nat.add n (Init.Nat.sub (@fst nat nat x) (S n)))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl;omega.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  rewrite e;left;exists (1,0);simpl;rewrite <- minus_n_O;rewrite plus_comm;simpl;apply gcd_refl.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (@snd nat nat x))) (@fst nat nat x) (@snd nat nat x))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (@snd nat nat x)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (@snd nat nat x))) *)
  destruct (snd x).
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) O)) (@fst nat nat x) O)) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) O) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) O)) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (S n))) (@fst nat nat x) (S n))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (S n)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (S n))) *)
  left;exists (1,0);simpl;rewrite <- minus_n_O;rewrite plus_comm;simpl;apply gcd_sym;apply gcd_zero.
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (S n))) (@fst nat nat x) (S n))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (S n)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (S n))) *)
  elim (H (S n,fst x-S n));try (intro;simpl).
(* Goal: not (@eq nat d O) *)
  elim a;intro y;intro.
(* Goal: is_gcd d (@fst nat nat x) (@snd nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat x) (remainder_euclide (@snd nat nat x) (@fst nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  right;exists ((snd y),(fst y)+(snd y));apply gcd_sym.
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (S n)) (Init.Nat.mul (@fst nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (@fst nat nat x))) (S n) (@fst nat nat x) *)
(* Goal: sum (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat y) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat y) (S n))) (@fst nat nat x) (S n))) (@sig (prod nat nat) (fun y : prod nat nat => is_gcd (Init.Nat.sub (Init.Nat.mul (@snd nat nat y) (S n)) (Init.Nat.mul (@fst nat nat y) (@fst nat nat x))) (@fst nat nat x) (S n))) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl;apply bezout_aux1;try (auto with arith).
(* Goal: not (@eq nat d O) *)
  elim b;intro y;intro.
(* Goal: is_gcd d (@fst nat nat x) (@snd nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat x) (remainder_euclide (@snd nat nat x) (@fst nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  left;exists ((snd y),(fst y)+(snd y));apply gcd_sym.
(* Goal: is_gcd (Init.Nat.sub (Init.Nat.mul (@fst nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (@fst nat nat x)) (Init.Nat.mul (@snd nat nat (@pair nat nat (@snd nat nat y) (Init.Nat.add (@fst nat nat y) (@snd nat nat y)))) (S n))) (S n) (@fst nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl;apply bezout_aux2;try (auto with arith).
(* Goal: lt (S (Init.Nat.add n (Init.Nat.sub (@fst nat nat x) (S n)))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  simpl;omega.
Qed.

(** Bezout' theorem *)
Theorem bezout_exists : forall (a b:nat),{u:nat & {v:nat | (is_gcd (a*u-b*v) a b)}}+{u:nat & {v:nat | (is_gcd (b*v-a*u) a b)}}.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  elim (bezout_exists_prod (a,b));intro.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim a0;destruct x;simpl;intros.
(* Goal: sum (@sigT nat (fun u : nat => @sig nat (fun v : nat => is_gcd (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v)) a b))) (@sigT nat (fun u : nat => @sig nat (fun v : nat => is_gcd (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u)) a b))) *)
(* Goal: sum (@sigT nat (fun u : nat => @sig nat (fun v : nat => is_gcd (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v)) a b))) (@sigT nat (fun u : nat => @sig nat (fun v : nat => is_gcd (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u)) a b))) *)
  left;exists n;exists n0;rewrite mult_comm;rewrite (mult_comm b);trivial.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim b0;destruct x;simpl;intros.
(* Goal: sum (@sigT nat (fun u : nat => @sig nat (fun v : nat => is_gcd (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v)) a b))) (@sigT nat (fun u : nat => @sig nat (fun v : nat => is_gcd (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u)) a b))) *)
  right;exists n;exists n0;rewrite mult_comm;rewrite (mult_comm a);trivial.
Qed.

(** Bezout' theorem reformulated *)
Theorem bezout : forall (d a b:nat),(is_gcd d a b)->exists u:nat,exists v:nat,d=a*u-b*v \/ d=b*v-a*u.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  elim (bezout_exists a b);intro.
(* Goal: @ex nat (fun u : nat => @ex nat (fun v : nat => or (@eq nat d (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v))) (@eq nat d (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u))))) *)
(* Goal: @ex nat (fun u : nat => @ex nat (fun v : nat => or (@eq nat d (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v))) (@eq nat d (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u))))) *)
  elim a0;intro u;intro;elim p;intro v;intro;exists u;exists v;left;apply (gcd_unique d (a*u-b*v) a b);trivial.
(* Goal: @ex nat (fun u : nat => @ex nat (fun v : nat => or (@eq nat d (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v))) (@eq nat d (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u))))) *)
  elim b0;intro u;intro;elim p;intro v;intro;exists u;exists v;right;apply (gcd_unique d (b*v-a*u) a b);trivial.
Qed.

(** Bezout' theorem and relatively prime numbers *)
Theorem bezout_rel_prime : forall (a b:nat),(rel_prime a b)<->(exists u:nat, exists v:nat, 1=a*u-b*v \/ 1 = b*v-a*u).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: sumbool (rel_prime a b) (not (rel_prime a b)) *)
  unfold rel_prime.
(* Goal: not (@eq nat d O) *)
  split;intro.
(* Goal: @ex nat (fun u : nat => @ex nat (fun v : nat => or (@eq nat (S O) (Init.Nat.sub (Init.Nat.mul a u) (Init.Nat.mul b v))) (@eq nat (S O) (Init.Nat.sub (Init.Nat.mul b v) (Init.Nat.mul a u))))) *)
(* Goal: is_gcd (S O) a b *)
  apply bezout;trivial.
(* Goal: is_gcd (S O) a b *)
  elim H;intro u;intro H0.
(* Goal: not (@eq nat d O) *)
  elim H0;intro v;intro.
(* Goal: and (is_cd a a a) (forall (d' : nat) (_ : is_cd d' a a), divides a d') *)
  unfold is_gcd;unfold is_cd.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: and (divides a (S O)) (divides b (S O)) *)
(* Goal: forall (d' : nat) (_ : and (divides a d') (divides b d')), divides (S O) d' *)
  split;apply one_min_div.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H2;intros.
(* Goal: not (@eq nat d O) *)
  elim H3;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H4;intro q';intro.
(* Goal: divides (S O) d' *)
  rewrite H5 in H1;rewrite H6 in H1.
(* Goal: not (@eq nat d O) *)
  case H1;intro.
(* Goal: divides (S O) d' *)
(* Goal: divides (S O) d' *)
  exists (q*u-q'*v);rewrite mult_minus_lemma2;rewrite mult_assoc;rewrite mult_assoc;trivial.
(* Goal: divides (S O) d' *)
  exists (q'*v-q*u);rewrite mult_minus_lemma2;rewrite mult_assoc;rewrite mult_assoc;trivial.
Qed.

(** gcd(n*a,n*b) = n*gcd(a,b) *)
Lemma gcd_mult : forall (d a b:nat),(is_gcd d a b)->(forall (n:nat),(is_gcd (n*d) (n*a) (n*b))).
(* Goal: and (is_cd a a a) (forall (d' : nat) (_ : is_cd d' a a), divides a d') *)
  unfold is_gcd;unfold is_cd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H;intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H0;intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: not (@eq nat d O) *)
  elim H2;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H3;intro q';intro.
(* Goal: and (divides (Init.Nat.mul n a) (Init.Nat.mul n d)) (divides (Init.Nat.mul n b) (Init.Nat.mul n d)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.mul n a) d') (divides (Init.Nat.mul n b) d')), divides (Init.Nat.mul n d) d' *)
  rewrite H4;rewrite mult_assoc.
(* Goal: and (divides (Nat.mul (Nat.mul n d) q) (Init.Nat.mul n d)) (divides (Init.Nat.mul n b) (Init.Nat.mul n d)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.mul n a) d') (divides (Init.Nat.mul n b) d')), divides (Init.Nat.mul n d) d' *)
  rewrite H5;rewrite mult_assoc.
(* Goal: and (divides (Nat.mul (Nat.mul n d) q) (Init.Nat.mul n d)) (divides (Nat.mul (Nat.mul n d) q') (Init.Nat.mul n d)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.mul n a) d') (divides (Init.Nat.mul n b) d')), divides (Init.Nat.mul n d) d' *)
  split;[exists q;trivial | exists q';trivial].
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H4;intros.
(* Goal: divides (Init.Nat.mul n d) d' *)
  elim (bezout d a b);try (unfold is_gcd;unfold is_cd;trivial).
(* Goal: not (@eq nat d O) *)
  intro u;intro.
(* Goal: not (@eq nat d O) *)
  elim H7;intro v;intro.
(* Goal: not (@eq nat d O) *)
  elim H5;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H6;intro q';intro.
(* Goal: divides (Init.Nat.mul n d) d' *)
  case H8;intro;[exists (q*u-q'*v) | exists (q'*v-q*u)];rewrite mult_minus_lemma2;rewrite mult_assoc;rewrite mult_assoc;rewrite <- H9;rewrite <- H10;rewrite H11;rewrite mult_minus_lemma2;rewrite mult_assoc;rewrite mult_assoc;trivial.
Qed.

(** Gauss' theorem (use Bezout) *)
Theorem gauss : forall (d a b:nat),(rel_prime a d)->(divides (a*b) d)->(divides b d).
(* Goal: sumbool (rel_prime a b) (not (rel_prime a b)) *)
  unfold rel_prime.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  elim (bezout 1 a d H);intro u;intro.
(* Goal: not (@eq nat d O) *)
  elim H1;intro v;intro.
(* Goal: not (@eq nat d O) *)
  elim H0;intro q;intro.
(* Goal: divides b d *)
  case H2;intro;[exists (q*u-b*v) | exists (b*v-q*u)];rewrite mult_minus_lemma2;rewrite mult_assoc;rewrite mult_assoc;rewrite <- H3;rewrite (mult_comm a b);rewrite (mult_comm d b);rewrite <- mult_assoc;rewrite <- mult_assoc;rewrite <- mult_minus_lemma2;rewrite <- H4;auto with arith.
Qed.

(** we show that if b<>0, then gcd(a,b)=gcd(b,a mod b) *)
Lemma gcd_euclide : forall (d a b:nat)(H:(b<>0)),(is_gcd d a b)<->(is_gcd d b (remainder_euclide a b H)).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: not (@eq nat d O) *)
  generalize (quo_rem_euclide a b H);intro.
(* Goal: not (@eq nat d O) *)
  red;split;intro.
(* Goal: is_gcd d b (remainder_euclide a b H) *)
(* Goal: is_gcd d a b *)
  rewrite H0 in H1.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H1;intros.
(* Goal: and (is_cd a a a) (forall (d' : nat) (_ : is_cd d' a a), divides a d') *)
  unfold is_gcd;unfold is_cd.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H2;intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: and (divides b d') (divides (remainder_euclide a b H) d') *)
  split;try tauto.
(* Goal: not (@eq nat d O) *)
  elim H4;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H5;intro q';intro.
(* Goal: divides (remainder_euclide a b H) d *)
(* Goal: forall (d' : nat) (_ : and (divides b d') (divides (remainder_euclide a b H) d')), divides d d' *)
(* Goal: is_gcd d a b *)
  replace (b*(quotient_euclide a b H)) with (d*q'*(quotient_euclide a b H)) in H6.
(* Goal: divides (remainder_euclide a b H) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q') (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides b d') (divides (remainder_euclide a b H) d')), divides d d' *)
(* Goal: is_gcd d a b *)
  assert ((remainder_euclide a b H)=(d*q-d*q'*(quotient_euclide a b H))).
(* Goal: @eq nat (remainder_euclide a b H) (Init.Nat.sub (Init.Nat.mul d q) (Init.Nat.mul (Init.Nat.mul d q') (quotient_euclide a b H))) *)
(* Goal: divides (remainder_euclide a b H) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q') (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides b d') (divides (remainder_euclide a b H) d')), divides d d' *)
(* Goal: is_gcd d a b *)
  rewrite <- H6;rewrite minus_plus;trivial.
(* Goal: divides (remainder_euclide a b H) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q') (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides b d') (divides (remainder_euclide a b H) d')), divides d d' *)
(* Goal: is_gcd d a b *)
  rewrite <- mult_assoc in H8;rewrite <- mult_minus_lemma2 in H8.
(* Goal: divides (remainder_euclide a b H) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q') (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides b d') (divides (remainder_euclide a b H) d')), divides d d' *)
(* Goal: is_gcd d a b *)
  exists (q-q'*(quotient_euclide a b H));trivial.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q') (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides b d') (divides (remainder_euclide a b H) d')), divides d d' *)
(* Goal: is_gcd d a b *)
  rewrite <- H7;trivial.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H6;intros.
(* Goal: divides d d' *)
  apply H3.
(* Goal: and (divides b d') (divides (remainder_euclide a b H) d') *)
  unfold is_cd;split;try tauto.
(* Goal: not (@eq nat d O) *)
  elim H7;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H8;intro q';intro.
(* Goal: divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d' *)
(* Goal: is_gcd d a b *)
  rewrite H10.
(* Goal: divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (Init.Nat.mul d' q')) d' *)
(* Goal: is_gcd d a b *)
  replace (b*(quotient_euclide a b H)) with (d'*q*(quotient_euclide a b H)).
(* Goal: divides (Init.Nat.add (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul d q')) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  rewrite <- mult_assoc;rewrite <- mult_plus_distr_l.
(* Goal: divides (Nat.mul d (Nat.add (Nat.mul q (quotient_euclide a b H)) q')) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  exists (q*(quotient_euclide a b H)+q');trivial.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d' q) (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: is_gcd d a b *)
  rewrite <- H9;trivial.
(* Goal: and (is_cd a a a) (forall (d' : nat) (_ : is_cd d' a a), divides a d') *)
  unfold is_gcd;unfold is_cd.
(* Goal: and (and (divides a d) (divides b d)) (forall (d' : nat) (_ : and (divides a d') (divides b d')), divides d d') *)
  unfold is_gcd in H1;unfold is_cd in H1.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H1;intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H2;intros.
(* Goal: and (and (divides a d) (divides b d)) (forall (d' : nat) (_ : and (divides a d') (divides b d')), divides d d') *)
  rewrite H0.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: and (divides b d') (divides (remainder_euclide a b H) d') *)
  split;try tauto.
(* Goal: not (@eq nat d O) *)
  elim H4;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H5;intro q';intro.
(* Goal: divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  rewrite H7.
(* Goal: divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (Init.Nat.mul d q')) d *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  replace (b*(quotient_euclide a b H)) with (d*q*(quotient_euclide a b H)).
(* Goal: divides (Init.Nat.add (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul d q')) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  rewrite <- mult_assoc;rewrite <- mult_plus_distr_l.
(* Goal: divides (Nat.mul d (Nat.add (Nat.mul q (quotient_euclide a b H)) q')) d *)
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  exists (q*(quotient_euclide a b H)+q');trivial.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) (quotient_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H)) *)
(* Goal: forall (d' : nat) (_ : and (divides (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) d') (divides b d')), divides d d' *)
  rewrite <- H6;trivial.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: divides d d' *)
  apply H3.
(* Goal: and (divides b d') (divides (remainder_euclide a b H) d') *)
  split;try tauto.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H6;intros.
(* Goal: not (@eq nat d O) *)
  elim H7;intro q;intro.
(* Goal: not (@eq nat d O) *)
  elim H8;intro q';intro.
(* Goal: divides (remainder_euclide a b H) d' *)
  assert ((remainder_euclide a b H)=b*(quotient_euclide a b H)+(remainder_euclide a b H)-b*(quotient_euclide a b H)).
(* Goal: @eq nat (remainder_euclide a b H) (Init.Nat.sub (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)) (Init.Nat.mul b (quotient_euclide a b H))) *)
(* Goal: divides (remainder_euclide a b H) d' *)
  rewrite minus_plus;trivial.
(* Goal: divides (remainder_euclide a b H) d' *)
  rewrite H9 in H11.
(* Goal: divides (remainder_euclide a b H) d' *)
  exists (q-q'*(quotient_euclide a b H)).
(* Goal: @eq nat (remainder_euclide a b H) (Init.Nat.mul d' (Init.Nat.sub q (Init.Nat.mul q' (quotient_euclide a b H)))) *)
  rewrite mult_minus_lemma2;rewrite mult_assoc.
(* Goal: @eq nat (remainder_euclide a b H) (Init.Nat.sub (Init.Nat.mul d' q) (Nat.mul (Nat.mul d' q') (quotient_euclide a b H))) *)
  rewrite <- H10;trivial.
Qed.

(** we give a "more efficient" algorithm to compute gcd(a,b) *)
Lemma gcd_exists_prod_bis : forall (x:nat*nat),{d:nat | (is_gcd d (fst x) (snd x))}.
(* Goal: forall x : prod nat nat, @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  apply (induction_ltof2 (nat*nat) f (fun x:nat*nat => {d:nat | (is_gcd d (fst x) (snd x))})).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  unfold ltof;unfold f;intros.
(* Goal: not (@eq nat d O) *)
  case (lt_eq_lt_dec (fst x) (snd x));intro.
(* Goal: not (@eq nat d O) *)
  case s;intro.
(* Goal: not (@eq nat d O) *)
  case (eq_nat_dec (fst x) 0);intro.
(* Goal: @sig nat (fun d : nat => is_gcd d O (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (S n) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  rewrite e;exists (snd x);apply gcd_zero.
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  elim (H ((fst x),(remainder_euclide (snd x) (fst x) n)));simpl.
(* Goal: not (@eq nat d O) *)
  intro d;intro.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: lt (Init.Nat.add (@snd nat nat x) (remainder_euclide (@fst nat nat x) (@snd nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
  exists d.
(* Goal: is_gcd d (@fst nat nat x) (@snd nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat x) (remainder_euclide (@snd nat nat x) (@fst nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  apply gcd_sym.
(* Goal: is_gcd d (@snd nat nat x) (@fst nat nat x) *)
(* Goal: lt (Init.Nat.add (@fst nat nat x) (remainder_euclide (@snd nat nat x) (@fst nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  elim (gcd_euclide d (snd x) (fst x) n);auto.
(* Goal: lt (S (Init.Nat.add n (Init.Nat.sub (@fst nat nat x) (S n)))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  generalize (rem_euclide (snd x) (fst x) n);try omega.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
  rewrite e;exists (snd x);apply gcd_refl.
(* Goal: not (@eq nat d O) *)
  case (eq_nat_dec (snd x) 0);intro.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) O) *)
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (S n)) *)
  rewrite e;exists (fst x);apply gcd_sym;apply gcd_zero.
(* Goal: lt (Init.Nat.add (@fst nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n)))) (@snd nat nat (@pair nat nat (S n) (Init.Nat.sub (@fst nat nat x) (S n))))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  elim (H ((snd x),(remainder_euclide (fst x) (snd x) n)));simpl.
(* Goal: not (@eq nat d O) *)
  intro d;intro.
(* Goal: @sig nat (fun d : nat => is_gcd d (@fst nat nat x) (@snd nat nat x)) *)
(* Goal: lt (Init.Nat.add (@snd nat nat x) (remainder_euclide (@fst nat nat x) (@snd nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
  exists d.
(* Goal: is_gcd d (@fst nat nat x) (@snd nat nat x) *)
(* Goal: lt (Init.Nat.add (@snd nat nat x) (remainder_euclide (@fst nat nat x) (@snd nat nat x) n)) (Init.Nat.add (@fst nat nat x) (@snd nat nat x)) *)
  elim (gcd_euclide d (fst x) (snd x) n);auto.
(* Goal: lt (S (Init.Nat.add n (Init.Nat.sub (@fst nat nat x) (S n)))) (Init.Nat.add (@fst nat nat x) (S n)) *)
  generalize (rem_euclide (fst x) (snd x) n);try omega.
Qed.

(** efficient algorithm to compute gcd(a,b) *)
Theorem gcd_exists_bis : forall (a b:nat),{d:nat | (is_gcd d a b)}.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim (gcd_exists_prod_bis (a,b));intro d;simpl;intros.
(* Goal: @sig nat (fun d : nat => is_gcd d a b) *)
  exists d;trivial.
Qed.

(** it is decidable to say if a and b are relatively prime *)
Lemma rel_prime_dec : forall (a b:nat),{rel_prime a b}+{~(rel_prime a b)}.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: sumbool (rel_prime a b) (not (rel_prime a b)) *)
  unfold rel_prime.
(* Goal: not (@eq nat d O) *)
  generalize (gcd_is_gcd a b);intro.
(* Goal: not (@eq nat d O) *)
  case (eq_nat_dec (gcd a b) 1);intro.
(* Goal: sumbool (is_gcd (S O) a b) (not (is_gcd (S O) a b)) *)
(* Goal: sumbool (is_gcd (S O) a b) (not (is_gcd (S O) a b)) *)
  left;rewrite e in H;trivial.
(* Goal: sumbool (is_gcd (S O) a b) (not (is_gcd (S O) a b)) *)
  right;intro;apply n;apply (gcd_unique (gcd a b) 1 a b);trivial.
Qed.

(** if gcd(a,b)=1 and gcd(a,c)=1 then gcd(a,b*c)=1 *)
Lemma rel_prime_mult : forall (a b c:nat),(rel_prime a b)->(rel_prime a c)->(rel_prime a (b*c)).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: rel_prime a (Init.Nat.mul b c) *)
  split.
(* Goal: is_cd (S O) a (Init.Nat.mul b c) *)
(* Goal: forall (d' : nat) (_ : is_cd d' a (Init.Nat.mul b c)), divides (S O) d' *)
  split;try (apply one_min_div).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H1;intros.
(* Goal: not (@eq nat d O) *)
  case (rel_prime_dec b d');intro.
(* Goal: divides (S O) d' *)
(* Goal: divides (S O) d' *)
  assert (divides c d').
(* Goal: divides c d' *)
(* Goal: divides (S O) d' *)
(* Goal: divides (S O) d' *)
  apply gauss with b;trivial.
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  elim H0;intros.
(* Goal: forall (d' : nat) (_ : is_cd d' (S O) a), divides (S O) d' *)
  apply H6;unfold is_cd;tauto.
(* Goal: not (@eq nat d O) *)
  generalize (gcd_is_gcd b d');intro.
(* Goal: divides (S O) d' *)
  assert ((gcd b d')<>1).
(* Goal: not (@eq nat (gcd b d') (S O)) *)
(* Goal: divides (S O) d' *)
  intro;apply n.
(* Goal: rel_prime b d' *)
(* Goal: divides (S O) d' *)
  unfold rel_prime;rewrite <- H5;trivial.
(* Goal: not (@eq nat d O) *)
  generalize (gcd_div_l (gcd b d') b d' H4);intro.
(* Goal: not (@eq nat d O) *)
  generalize (gcd_div_r (gcd b d') b d' H4);intro.
(* Goal: divides (S O) d' *)
  assert (divides a (gcd b d')).
(* Goal: divides a (gcd b d') *)
(* Goal: divides (S O) d' *)
  apply divides_trans with d';[apply H2 | apply H7].
(* Goal: divides (S O) d' *)
  elim H5.
(* Goal: @eq nat (gcd b d') (S O) *)
  apply divides_antisym.
(* Goal: divides (gcd b d') (S O) *)
(* Goal: divides (S O) (gcd b d') *)
  apply one_min_div.
(* Goal: forall (d' : nat) (_ : is_cd d' (S O) a), divides (S O) d' *)
  elim H;intros;apply H10;unfold is_cd;tauto.
Qed.

(** if gcd(a,b*c)=1 then gcd(a,b)=1 and gcd(a,c)=1 *)
Lemma mult_rel_prime : forall (a b c:nat),(rel_prime a (b*c))->((rel_prime a b)/\(rel_prime a c)).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  intros.
(* Goal: and (rel_prime a b) (rel_prime a c) *)
  split;split;[split | intros | split | intros];try (apply one_min_div);elim H0;intros;elim H;intros;apply H4;split;trivial;elim H2;intro q;intro;rewrite H5;[exists (q*c) | exists (q*b)];ring.
Qed.

(** if gcd(a,d)=1 then gcd(a,d^n)=1 *)
Lemma rel_prime_power : forall (d a n:nat),(rel_prime a d)->(rel_prime a (power d n)).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  induction n;simpl;intros.
(* Goal: rel_prime a (S O) *)
(* Goal: rel_prime a (Init.Nat.mul d (power d n)) *)
  unfold rel_prime;apply gcd_sym;apply gcd_one.
(* Goal: not (@eq nat d O) *)
  generalize (IHn H);intro.
(* Goal: rel_prime a (Init.Nat.mul d (power d n)) *)
  apply rel_prime_mult;trivial.
Qed.

(** if n>0 and gcd(a,d^n)=1 then gcd(a,d)=1 *)
Lemma power_rel_prime : forall (d a n:nat),(n>0)->(rel_prime a (power d n))->(rel_prime a d).
(* Goal: forall (a b c : nat) (_ : rel_prime a (Init.Nat.mul b c)), and (rel_prime a b) (rel_prime a c) *)
  destruct n;simpl;intros.
(* Goal: rel_prime a d *)
(* Goal: rel_prime a d *)
  inversion H.
(* Goal: rel_prime a d *)
  elim (mult_rel_prime a d (power d n));auto.
Qed.

(** if n>0 and m>0 then gcd(a^n,b^m)=1 iff gcd(a,b)=1 *)
Lemma power_power_rel_prime : forall (a n b m:nat),(n>0)->(m>0)->((rel_prime (power a n) (power b m))<->(rel_prime a b)).
(* Goal: not (@eq nat d O) *)
  split;intro.
(* Goal: rel_prime a b *)
(* Goal: rel_prime (power a n) (power b m) *)
  apply power_rel_prime with m;trivial;apply rel_prime_sym;apply power_rel_prime with n;trivial;apply rel_prime_sym;trivial.
(* Goal: rel_prime (power a n) (power b m) *)
  apply rel_prime_power;apply rel_prime_sym;apply rel_prime_power;apply rel_prime_sym;trivial.
Qed.

