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

Zgcd_alt : an alternate version of Z.gcd, based on Euclid's algorithm

Author: Pierre Letouzey

The alternate Zgcd_alt given here used to be the main Z.gcd function (see file Znumtheory), but this main Z.gcd is now based on a modern binary-efficient algorithm. This earlier version, based on Euclid's algorithm of iterated modulo, is kept here due to both its intrinsic interest and its use as reference point when proving gcd on Int31 numbers

Require Import ZArith_base.
Require Import ZArithRing.
Require Import Zdiv.
Require Import Znumtheory.
Require Import Omega.

Open Scope Z_scope.

In Coq, we need to control the number of iteration of modulo. For that, we use an explicit measure in nat, and we prove later that using 2*d is enough, where d is the number of binary digits of the first argument.

 Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b =>
   match n with
     | O => 1 (* arbitrary, since n should be big enough *)
     | S n => match a with
	        | Z0 => Z.abs b
	        | Zpos _ => Zgcdn n (Z.modulo b a) a
	        | Zneg a => Zgcdn n (Z.modulo b (Zpos a)) (Zpos a)
  	      end
   end.

 Definition Zgcd_bound (a:Z) :=
   match a with
     | Z0 => S O
     | Zpos p => let n := Pos.size_nat p in (n+n)%nat
     | Zneg p => let n := Pos.size_nat p in (n+n)%nat
   end.

 Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b.

A first obvious fact : Z.gcd a b is positive.

 Lemma Zgcdn_pos : forall n a b,
   0 <= Zgcdn n a b.forall (n : nat) (a b : Z), 0 <= Zgcdn n a b
 Proof.forall (n : nat) (a b : Z), 0 <= Zgcdn n a b
   induction n.forall a b : Z, 0 <= Zgcdn 0 a b
n:nat
IHn:forall a b : Z, 0 <= Zgcdn n a b
forall a b : Z, 0 <= Zgcdn (S n) a b
   simpl; auto with zarith.n:nat
IHn:forall a b : Z, 0 <= Zgcdn n a b
forall a b : Z, 0 <= Zgcdn (S n) a b
   destruct a; simpl; intros; auto with zarith; auto.
 Qed.

 Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b.forall a b : Z, 0 <= Zgcd_alt a b
 Proof.forall a b : Z, 0 <= Zgcd_alt a b
   intros; unfold Z.gcd; apply Zgcdn_pos; auto.
 Qed.

We now prove that Z.gcd is indeed a gcd.

1) We prove a weaker & easier bound.

 Lemma Zgcdn_linear_bound : forall n a b,
   Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b).forall (n : nat) (a b : Z),
Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b)
 Proof.forall (n : nat) (a b : Z),
Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b)
   induction n.forall a b : Z,
Z.abs a < Z.of_nat 0 -> Zis_gcd a b (Zgcdn 0 a b)
n:nat
IHn:forall a b : Z, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b)
forall a b : Z,
Z.abs a < Z.of_nat (S n) ->
Zis_gcd a b (Zgcdn (S n) a b)
   simpl; intros.a, b:Z
H:Z.abs a < 0
Zis_gcd a b 1
n:nat
IHn:forall a b : Z, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b)
forall a b : Z,
Z.abs a < Z.of_nat (S n) ->
Zis_gcd a b (Zgcdn (S n) a b)
   exfalso; generalize (Z.abs_nonneg a); omega.n:nat
IHn:forall a b : Z, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b)
forall a b : Z,
Z.abs a < Z.of_nat (S n) ->
Zis_gcd a b (Zgcdn (S n) a b)
   destruct a; intros; simpl;
     [ generalize (Zis_gcd_0_abs b); intuition | | ];
   unfold Z.modulo;
   generalize (Z_div_mod b (Zpos p) (eq_refl Gt));
   destruct (Z.div_eucl b (Zpos p)) as (q,r);
   intros (H0,H1);
   rewrite Nat2Z.inj_succ in H; simpl Z.abs in H;
   (assert (H2: Z.abs r < Z.of_nat n) by
    (rewrite Z.abs_eq; auto with zarith));
    assert (IH:=IHn r (Zpos p) H2); clear IHn;
    simpl in IH |- *;
    rewrite H0.n:nat
p:positive
b:Z
H:Z.pos p < Z.succ (Z.of_nat n)
q, r:Z
H0:b = Z.pos p * q + r
H1:0 <= r < Z.pos p
H2:Z.abs r < Z.of_nat n
IH:Zis_gcd r (Z.pos p) (Zgcdn n r (Z.pos p))
Zis_gcd (Z.pos p) (Z.pos p * q + r)
  (Zgcdn n r (Z.pos p))
n:nat
p:positive
b:Z
H:Z.pos p < Z.succ (Z.of_nat n)
q, r:Z
H0:b = Z.pos p * q + r
H1:0 <= r < Z.pos p
H2:Z.abs r < Z.of_nat n
IH:Zis_gcd r (Z.pos p) (Zgcdn n r (Z.pos p))
Zis_gcd (Z.neg p) (Z.pos p * q + r)
  (Zgcdn n r (Z.pos p))
   apply Zis_gcd_for_euclid2; auto.n:nat
p:positive
b:Z
H:Z.pos p < Z.succ (Z.of_nat n)
q, r:Z
H0:b = Z.pos p * q + r
H1:0 <= r < Z.pos p
H2:Z.abs r < Z.of_nat n
IH:Zis_gcd r (Z.pos p) (Zgcdn n r (Z.pos p))
Zis_gcd (Z.neg p) (Z.pos p * q + r)
  (Zgcdn n r (Z.pos p))
   apply Zis_gcd_minus; apply Zis_gcd_sym.n:nat
p:positive
b:Z
H:Z.pos p < Z.succ (Z.of_nat n)
q, r:Z
H0:b = Z.pos p * q + r
H1:0 <= r < Z.pos p
H2:Z.abs r < Z.of_nat n
IH:Zis_gcd r (Z.pos p) (Zgcdn n r (Z.pos p))
Zis_gcd (- Z.neg p) (Z.pos p * q + r)
  (Zgcdn n r (Z.pos p))
   apply Zis_gcd_for_euclid2; auto.
 Qed.

2) For Euclid's algorithm, the worst-case situation corresponds to Fibonacci numbers. Let's define them:

 Fixpoint fibonacci (n:nat) : Z :=
   match n with
     | O => 1
     | S O => 1
     | S (S n as p) => fibonacci p + fibonacci n
   end.

 Lemma fibonacci_pos : forall n, 0 <= fibonacci n.forall n : nat, 0 <= fibonacci n
 Proof.forall n : nat, 0 <= fibonacci n
   enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto.forall N n : nat, (n < N)%nat -> 0 <= fibonacci n
   induction N.forall n : nat, (n < 0)%nat -> 0 <= fibonacci n
N:nat
IHN:forall n : nat, (n < N)%nat -> 0 <= fibonacci n
forall n : nat, (n < S N)%nat -> 0 <= fibonacci n
   inversion 1.N:nat
IHN:forall n : nat, (n < N)%nat -> 0 <= fibonacci n
forall n : nat, (n < S N)%nat -> 0 <= fibonacci n
   intros.N:nat
IHN:forall n0 : nat, (n0 < N)%nat -> 0 <= fibonacci n0
n:nat
H:(n < S N)%nat
0 <= fibonacci n
   destruct n.N:nat
IHN:forall n : nat, (n < N)%nat -> 0 <= fibonacci n
H:(0 < S N)%nat
0 <= fibonacci 0
N:nat
IHN:forall n0 : nat, (n0 < N)%nat -> 0 <= fibonacci n0
n:nat
H:(S n < S N)%nat
0 <= fibonacci (S n)
   simpl; auto with zarith.N:nat
IHN:forall n0 : nat, (n0 < N)%nat -> 0 <= fibonacci n0
n:nat
H:(S n < S N)%nat
0 <= fibonacci (S n)
   destruct n.N:nat
IHN:forall n : nat, (n < N)%nat -> 0 <= fibonacci n
H:(1 < S N)%nat
0 <= fibonacci 1
N:nat
IHN:forall n0 : nat, (n0 < N)%nat -> 0 <= fibonacci n0
n:nat
H:(S (S n) < S N)%nat
0 <= fibonacci (S (S n))
   simpl; auto with zarith.N:nat
IHN:forall n0 : nat, (n0 < N)%nat -> 0 <= fibonacci n0
n:nat
H:(S (S n) < S N)%nat
0 <= fibonacci (S (S n))
   change (0 <= fibonacci (S n) + fibonacci n).N:nat
IHN:forall n0 : nat, (n0 < N)%nat -> 0 <= fibonacci n0
n:nat
H:(S (S n) < S N)%nat
0 <= fibonacci (S n) + fibonacci n
   generalize (IHN n) (IHN (S n)); omega.
 Qed.

 Lemma fibonacci_incr :
   forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.forall n m : nat,
(n <= m)%nat -> fibonacci n <= fibonacci m
 Proof.forall n m : nat,
(n <= m)%nat -> fibonacci n <= fibonacci m
   induction 1.n:nat
fibonacci n <= fibonacci n
n, m:nat
H:(n <= m)%nat
IHle:fibonacci n <= fibonacci m
fibonacci n <= fibonacci (S m)
   auto with zarith.n, m:nat
H:(n <= m)%nat
IHle:fibonacci n <= fibonacci m
fibonacci n <= fibonacci (S m)
   apply Z.le_trans with (fibonacci m); auto.n, m:nat
H:(n <= m)%nat
IHle:fibonacci n <= fibonacci m
fibonacci m <= fibonacci (S m)
   clear.m:nat
fibonacci m <= fibonacci (S m)
   destruct m.fibonacci 0 <= fibonacci 1
m:nat
fibonacci (S m) <= fibonacci (S (S m))
   simpl; auto with zarith.m:nat
fibonacci (S m) <= fibonacci (S (S m))
   change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).m:nat
fibonacci (S m) <= fibonacci (S m) + fibonacci m
   generalize (fibonacci_pos m); omega.
 Qed.

3) We prove that fibonacci numbers are indeed worst-case: for a given number n, if we reach a conclusion about gcd(a,b) in exactly n+1 loops, then fibonacci (n+1)<=a ∧ fibonacci(n+2)<=b

 Lemma Zgcdn_worst_is_fibonacci : forall n a b,
   0 < a < b ->
   Zis_gcd a b (Zgcdn (S n) a b) ->
   Zgcdn n a b <> Zgcdn (S n) a b ->
   fibonacci (S n) <= a /\
   fibonacci (S (S n)) <= b.forall (n : nat) (a b : Z),
0 < a < b ->
Zis_gcd a b (Zgcdn (S n) a b) ->
Zgcdn n a b <> Zgcdn (S n) a b ->
fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b
 Proof.forall (n : nat) (a b : Z),
0 < a < b ->
Zis_gcd a b (Zgcdn (S n) a b) ->
Zgcdn n a b <> Zgcdn (S n) a b ->
fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b
   induction n.forall a b : Z,
0 < a < b ->
Zis_gcd a b (Zgcdn 1 a b) ->
Zgcdn 0 a b <> Zgcdn 1 a b ->
fibonacci 1 <= a /\ fibonacci 2 <= b
n:nat
IHn:forall a b : Z,
0 < a < b ->
Zis_gcd a b (Zgcdn (S n) a b) ->
Zgcdn n a b <> Zgcdn (S n) a b ->
fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b
forall a b : Z,
0 < a < b ->
Zis_gcd a b (Zgcdn (S (S n)) a b) ->
Zgcdn (S n) a b <> Zgcdn (S (S n)) a b ->
fibonacci (S (S n)) <= a /\
fibonacci (S (S (S n))) <= b
   intros [|a|a]; intros; simpl; omega.n:nat
IHn:forall a b : Z,
0 < a < b ->
Zis_gcd a b (Zgcdn (S n) a b) ->
Zgcdn n a b <> Zgcdn (S n) a b ->
fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b
forall a b : Z,
0 < a < b ->
Zis_gcd a b (Zgcdn (S (S n)) a b) ->
Zgcdn (S n) a b <> Zgcdn (S (S n)) a b ->
fibonacci (S (S n)) <= a /\
fibonacci (S (S (S n))) <= b
   intros [|a|a] b (Ha,Ha'); [simpl; omega | | easy ].n:nat
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn (S n) a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn (S n) a0 b0 ->
fibonacci (S n) <= a0 /\ fibonacci (S (S n)) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
Zis_gcd (Z.pos a) b (Zgcdn (S (S n)) (Z.pos a) b) ->
Zgcdn (S n) (Z.pos a) b <> Zgcdn (S (S n)) (Z.pos a) b ->
fibonacci (S (S n)) <= Z.pos a /\
fibonacci (S (S (S n))) <= b
   remember (S n) as m.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
Zis_gcd (Z.pos a) b (Zgcdn (S m) (Z.pos a) b) ->
Zgcdn m (Z.pos a) b <> Zgcdn (S m) (Z.pos a) b ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
   rewrite Heqm at 2.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
Zis_gcd (Z.pos a) b (Zgcdn (S m) (Z.pos a) b) ->
Zgcdn (S n) (Z.pos a) b <> Zgcdn (S m) (Z.pos a) b ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b simpl Zgcdn.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
Zis_gcd (Z.pos a) b
  (Zgcdn m (b mod Z.pos a) (Z.pos a)) ->
Zgcdn n (b mod Z.pos a) (Z.pos a) <>
Zgcdn m (b mod Z.pos a) (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
   unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl).n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
(let (q, r) := Z.div_eucl b (Z.pos a) in
 b = Z.pos a * q + r /\ 0 <= r < Z.pos a) ->
Zis_gcd (Z.pos a) b
  (Zgcdn m (let (_, r) := Z.div_eucl b (Z.pos a) in r)
     (Z.pos a)) ->
Zgcdn n (let (_, r) := Z.div_eucl b (Z.pos a) in r)
  (Z.pos a) <>
Zgcdn m (let (_, r) := Z.div_eucl b (Z.pos a) in r)
  (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
   destruct (Z.div_eucl b (Zpos a)) as (q,r).n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
b = Z.pos a * q + r /\ 0 <= r < Z.pos a ->
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
   intros (EQ,(Hr,Hr')).n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 <= r
Hr':r < Z.pos a
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
   Z.le_elim Hr.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 = r
Hr':r < Z.pos a
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
   - (* r > 0 *)n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
     replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\
fibonacci (S m) + fibonacci m <= b
     intros.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
fibonacci (S m) <= Z.pos a /\
fibonacci (S m) + fibonacci m <= b
     destruct (IHn r (Zpos a) (conj Hr Hr')); auto.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
Zis_gcd r (Z.pos a) (Zgcdn m r (Z.pos a))
n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
fibonacci (S m) <= Z.pos a /\
fibonacci (S m) + fibonacci m <= b
     +n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
Zis_gcd r (Z.pos a) (Zgcdn m r (Z.pos a)) assert (EQ' : r = Zpos a * (-q) + b) by (rewrite EQ; ring).n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
EQ':r = Z.pos a * - q + b
Zis_gcd r (Z.pos a) (Zgcdn m r (Z.pos a))
       rewrite EQ' at 1.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
EQ':r = Z.pos a * - q + b
Zis_gcd (Z.pos a * - q + b) 
  (Z.pos a) (Zgcdn m r (Z.pos a))
       apply Zis_gcd_sym.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
EQ':r = Z.pos a * - q + b
Zis_gcd (Z.pos a) (Z.pos a * - q + b)
  (Zgcdn m r (Z.pos a))
       apply Zis_gcd_for_euclid2; auto.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
EQ':r = Z.pos a * - q + b
Zis_gcd b (Z.pos a) (Zgcdn m r (Z.pos a))
       apply Zis_gcd_sym; auto.
     +n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
fibonacci (S m) <= Z.pos a /\
fibonacci (S m) + fibonacci m <= b split; auto.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
fibonacci (S m) + fibonacci m <= b
       rewrite EQ.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
fibonacci (S m) + fibonacci m <= Z.pos a * q + r
       apply Z.add_le_mono; auto.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
fibonacci (S m) <= Z.pos a * q
       apply Z.le_trans with (Zpos a * 1); auto.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
fibonacci (S m) <= Z.pos a * 1
n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
Z.pos a * 1 <= Z.pos a * q
       now rewrite Z.mul_1_r.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
Z.pos a * 1 <= Z.pos a * q
       apply Z.mul_le_mono_nonneg_l; auto with zarith.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
1 <= q
       change 1 with (Z.succ 0).n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
Z.succ 0 <= q apply Z.le_succ_l.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
0 < q
       destruct q; auto with zarith.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
p:positive
r:Z
EQ:b = Z.pos a * Z.neg p + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
0 < Z.neg p
       assert (Zpos a * Zneg p < 0) by now compute.n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
p:positive
r:Z
EQ:b = Z.pos a * Z.neg p + r
Hr:0 < r
Hr':r < Z.pos a
H:Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a))
H0:Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a)
H1:fibonacci m <= r
H2:fibonacci (S m) <= Z.pos a
H3:Z.pos a * Z.neg p < 0
0 < Z.neg p omega.
   - (* r = 0 *)n, m:nat
Heqm:m = S n
IHn:forall a0 b0 : Z,
0 < a0 < b0 ->
Zis_gcd a0 b0 (Zgcdn m a0 b0) ->
Zgcdn n a0 b0 <> Zgcdn m a0 b0 ->
fibonacci m <= a0 /\ fibonacci (S m) <= b0
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
EQ:b = Z.pos a * q + r
Hr:0 = r
Hr':r < Z.pos a
Zis_gcd (Z.pos a) b (Zgcdn m r (Z.pos a)) ->
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
     clear IHn EQ Hr'; intros _.n, m:nat
Heqm:m = S n
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q, r:Z
Hr:0 = r
Zgcdn n r (Z.pos a) <> Zgcdn m r (Z.pos a) ->
fibonacci (S m) <= Z.pos a /\ fibonacci (S (S m)) <= b
     subst r; simpl; rewrite Heqm.n, m:nat
Heqm:m = S n
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q:Z
Zgcdn n 0 (Z.pos a) <> Zgcdn (S n) 0 (Z.pos a) ->
fibonacci (S n) + fibonacci n <= Z.pos a /\
fibonacci (S n) + fibonacci n + fibonacci (S n) <= b
     destruct n.m:nat
Heqm:m = 1%nat
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q:Z
Zgcdn 0 0 (Z.pos a) <> Zgcdn 1 0 (Z.pos a) ->
fibonacci 1 + fibonacci 0 <= Z.pos a /\
fibonacci 1 + fibonacci 0 + fibonacci 1 <= b
n, m:nat
Heqm:m = S (S n)
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q:Z
Zgcdn (S n) 0 (Z.pos a) <> Zgcdn (S (S n)) 0 (Z.pos a) ->
fibonacci (S (S n)) + fibonacci (S n) <= Z.pos a /\
fibonacci (S (S n)) + fibonacci (S n) +
fibonacci (S (S n)) <= b
     +m:nat
Heqm:m = 1%nat
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q:Z
Zgcdn 0 0 (Z.pos a) <> Zgcdn 1 0 (Z.pos a) ->
fibonacci 1 + fibonacci 0 <= Z.pos a /\
fibonacci 1 + fibonacci 0 + fibonacci 1 <= b simpl.m:nat
Heqm:m = 1%nat
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q:Z
1 <> Z.pos a -> 2 <= Z.pos a /\ 3 <= b omega.
     +n, m:nat
Heqm:m = S (S n)
a:positive
b:Z
Ha:0 < Z.pos a
Ha':Z.pos a < b
q:Z
Zgcdn (S n) 0 (Z.pos a) <> Zgcdn (S (S n)) 0 (Z.pos a) ->
fibonacci (S (S n)) + fibonacci (S n) <= Z.pos a /\
fibonacci (S (S n)) + fibonacci (S n) +
fibonacci (S (S n)) <= b now destruct 1.
 Qed.

3b) We reformulate the previous result in a more positive way.

 Lemma Zgcdn_ok_before_fibonacci : forall n a b,
   0 < a < b -> a < fibonacci (S n) ->
   Zis_gcd a b (Zgcdn n a b).forall (n : nat) (a b : Z),
0 < a < b ->
a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b)
 Proof.forall (n : nat) (a b : Z),
0 < a < b ->
a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b)
   destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate].n:nat
p:positive
forall b : Z,
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   cut (forall k n b,
     k = (S (Pos.to_nat p) - n)%nat ->
     0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
     Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)).n:nat
p:positive
(forall (k n0 : nat) (b : Z),
 k = (S (Pos.to_nat p) - n0)%nat ->
 0 < Z.pos p < b ->
 Z.pos p < fibonacci (S n0) ->
 Zis_gcd (Z.pos p) b (Zgcdn n0 (Z.pos p) b)) ->
forall b : Z,
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
n:nat
p:positive
forall (k n0 : nat) (b : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n0) ->
Zis_gcd (Z.pos p) b (Zgcdn n0 (Z.pos p) b)
   destruct 2; eauto.n:nat
p:positive
forall (k n0 : nat) (b : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n0) ->
Zis_gcd (Z.pos p) b (Zgcdn n0 (Z.pos p) b)
   clear n; induction k.p:positive
forall (n : nat) (b : Z),
0%nat = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   intros.p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   assert (Pos.to_nat p < n)%nat by omega.p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:(Pos.to_nat p < n)%nat
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   apply Zgcdn_linear_bound.p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:(Pos.to_nat p < n)%nat
Z.abs (Z.pos p) < Z.of_nat n
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   simpl.p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:(Pos.to_nat p < n)%nat
Z.pos p < Z.of_nat n
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   generalize (inj_le _ _ H2).p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:(Pos.to_nat p < n)%nat
Z.of_nat (S (Pos.to_nat p)) <= Z.of_nat n ->
Z.pos p < Z.of_nat n
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   rewrite Nat2Z.inj_succ.p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:(Pos.to_nat p < n)%nat
Z.succ (Z.of_nat (Pos.to_nat p)) <= Z.of_nat n ->
Z.pos p < Z.of_nat n
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   rewrite positive_nat_Z; auto.p:positive
n:nat
b:Z
H:0%nat = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:(Pos.to_nat p < n)%nat
Z.succ (Z.pos p) <= Z.of_nat n -> Z.pos p < Z.of_nat n
p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   omega.p:positive
k:nat
IHk:forall (n : nat) (b : Z),
k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) -> Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
forall (n : nat) (b : Z),
S k = (S (Pos.to_nat p) - n)%nat ->
0 < Z.pos p < b ->
Z.pos p < fibonacci (S n) ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   intros.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
H3:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   apply IHk; auto.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
k = (S (Pos.to_nat p) - S n)%nat
p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
Z.pos p < fibonacci (S (S n))
p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
H3:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   omega.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
Z.pos p < fibonacci (S (S n))
p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
H3:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
Z.pos p < fibonacci (S n) + fibonacci n
p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
H3:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   generalize (fibonacci_pos n); omega.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
H3:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
   replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.p:positive
k:nat
IHk:forall (n0 : nat) (b0 : Z),
k = (S (Pos.to_nat p) - n0)%nat ->
0 < Z.pos p < b0 ->
Z.pos p < fibonacci (S n0) -> Zis_gcd (Z.pos p) b0 (Zgcdn n0 (Z.pos p) b0)
n:nat
b:Z
H:S k = (S (Pos.to_nat p) - n)%nat
H0:0 < Z.pos p < b
H1:Z.pos p < fibonacci (S n)
H2:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b) ->
Zgcdn n (Z.pos p) b <> Zgcdn (S n) (Z.pos p) b ->
fibonacci (S n) <= Z.pos p /\
fibonacci (S (S n)) <= b
H3:Zis_gcd (Z.pos p) b (Zgcdn (S n) (Z.pos p) b)
Zgcdn (S n) (Z.pos p) b = Zgcdn n (Z.pos p) b
   generalize (H2 H3); clear H2 H3; omega.
 Qed.

4) The proposed bound leads to a fibonacci number that is big enough.

 Lemma Zgcd_bound_fibonacci :
   forall a, 0 < a -> a < fibonacci (Zgcd_bound a).forall a : Z, 0 < a -> a < fibonacci (Zgcd_bound a)
 Proof.forall a : Z, 0 < a -> a < fibonacci (Zgcd_bound a)
   destruct a; [omega| | intro H; discriminate].p:positive
0 < Z.pos p ->
Z.pos p < fibonacci (Zgcd_bound (Z.pos p))
   intros _.p:positive
Z.pos p < fibonacci (Zgcd_bound (Z.pos p))
   induction p; [ | | compute; auto ];
    simpl Zgcd_bound in *;
    rewrite plus_comm; simpl plus;
    set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl;
    assert (n <> O) by (unfold n; destruct p; simpl; auto).p:positive
n:=(Pos.size_nat p + Pos.size_nat p)%nat:nat
IHp:Z.pos p < fibonacci n
H:n <> 0%nat
Z.pos p~1 <
match n with
| 0%nat => 1
| S n0 => fibonacci n + fibonacci n0
end + fibonacci n
p:positive
n:=(Pos.size_nat p + Pos.size_nat p)%nat:nat
IHp:Z.pos p < fibonacci n
H:n <> 0%nat
Z.pos p~0 <
match n with
| 0%nat => 1
| S n0 => fibonacci n + fibonacci n0
end + fibonacci n

   destruct n as [ |m]; [elim H; auto| ].p:positive
m:nat
IHp:Z.pos p < fibonacci (S m)
H:S m <> 0%nat
Z.pos p~1 <
fibonacci (S m) + fibonacci m + fibonacci (S m)
p:positive
n:=(Pos.size_nat p + Pos.size_nat p)%nat:nat
IHp:Z.pos p < fibonacci n
H:n <> 0%nat
Z.pos p~0 <
match n with
| 0%nat => 1
| S n0 => fibonacci n + fibonacci n0
end + fibonacci n
   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; omega.p:positive
n:=(Pos.size_nat p + Pos.size_nat p)%nat:nat
IHp:Z.pos p < fibonacci n
H:n <> 0%nat
Z.pos p~0 <
match n with
| 0%nat => 1
| S n0 => fibonacci n + fibonacci n0
end + fibonacci n

   destruct n as [ |m]; [elim H; auto| ].p:positive
m:nat
IHp:Z.pos p < fibonacci (S m)
H:S m <> 0%nat
Z.pos p~0 <
fibonacci (S m) + fibonacci m + fibonacci (S m)
   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; omega.
 Qed.

 (* 5) the end: we glue everything together and take care of
    situations not corresponding to [0<a<b]. *)

 Lemma Zgcd_bound_opp a : Zgcd_bound (-a) = Zgcd_bound a.a:Z
Zgcd_bound (- a) = Zgcd_bound a
 Proof.a:Z
Zgcd_bound (- a) = Zgcd_bound a
  now destruct a.
 Qed.

 Lemma Zgcdn_opp n a b : Zgcdn n (-a) b = Zgcdn n a b.n:nat
a, b:Z
Zgcdn n (- a) b = Zgcdn n a b
 Proof.n:nat
a, b:Z
Zgcdn n (- a) b = Zgcdn n a b
  induction n; simpl; auto.n:nat
a, b:Z
IHn:Zgcdn n (- a) b = Zgcdn n a b
match - a with
| 0 => Z.abs b
| Z.pos _ => Zgcdn n (b mod - a) (- a)
| Z.neg a0 => Zgcdn n (b mod Z.pos a0) (Z.pos a0)
end =
match a with
| 0 => Z.abs b
| Z.pos _ => Zgcdn n (b mod a) a
| Z.neg a0 => Zgcdn n (b mod Z.pos a0) (Z.pos a0)
end
  destruct a; simpl; auto.
 Qed.

 Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat ->
   Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b).n:nat
a:positive
b:Z
(Zgcd_bound (Z.pos a) <= n)%nat ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
 Proof.n:nat
a:positive
b:Z
(Zgcd_bound (Z.pos a) <= n)%nat ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  intros.n:nat
a:positive
b:Z
H:(Zgcd_bound (Z.pos a) <= n)%nat
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  generalize (Zgcd_bound_fibonacci (Zpos a)).n:nat
a:positive
b:Z
H:(Zgcd_bound (Z.pos a) <= n)%nat
(0 < Z.pos a ->
 Z.pos a < fibonacci (Zgcd_bound (Z.pos a))) ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  simpl Zgcd_bound in *.n:nat
a:positive
b:Z
H:(Pos.size_nat a + Pos.size_nat a <= n)%nat
(0 < Z.pos a ->
 Z.pos a < fibonacci (Pos.size_nat a + Pos.size_nat a)) ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  remember (Pos.size_nat a+Pos.size_nat a)%nat as m.n:nat
a:positive
b:Z
m:nat
Heqm:m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(m <= n)%nat
(0 < Z.pos a -> Z.pos a < fibonacci m) ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  assert (1 < m)%nat.n:nat
a:positive
b:Z
m:nat
Heqm:m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(m <= n)%nat
(1 < m)%nat
n:nat
a:positive
b:Z
m:nat
Heqm:m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(m <= n)%nat
H0:(1 < m)%nat
(0 < Z.pos a -> Z.pos a < fibonacci m) ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  {n:nat
a:positive
b:Z
m:nat
Heqm:m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(m <= n)%nat
(1 < m)%nat rewrite Heqm; destruct a; simpl; rewrite 1?plus_comm;
    auto with arith. }n:nat
a:positive
b:Z
m:nat
Heqm:m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(m <= n)%nat
H0:(1 < m)%nat
(0 < Z.pos a -> Z.pos a < fibonacci m) ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  destruct m as [ |m]; [inversion H0; auto| ].n:nat
a:positive
b:Z
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= n)%nat
H0:(1 < S m)%nat
(0 < Z.pos a -> Z.pos a < fibonacci (S m)) ->
Zis_gcd (Z.pos a) b (Zgcdn n (Z.pos a) b)
  destruct n as [ |n]; [inversion H; auto| ].n:nat
a:positive
b:Z
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
(0 < Z.pos a -> Z.pos a < fibonacci (S m)) ->
Zis_gcd (Z.pos a) b (Zgcdn (S n) (Z.pos a) b)
  simpl Zgcdn.n:nat
a:positive
b:Z
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
(0 < Z.pos a -> Z.pos a < fibonacci (S m)) ->
Zis_gcd (Z.pos a) b
  (Zgcdn n (b mod Z.pos a) (Z.pos a))
  unfold Z.modulo.n:nat
a:positive
b:Z
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
(0 < Z.pos a -> Z.pos a < fibonacci (S m)) ->
Zis_gcd (Z.pos a) b
  (Zgcdn n (let (_, r) := Z.div_eucl b (Z.pos a) in r)
     (Z.pos a))
  generalize (Z_div_mod b (Zpos a) (eq_refl Gt)).n:nat
a:positive
b:Z
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
(let (q, r) := Z.div_eucl b (Z.pos a) in
 b = Z.pos a * q + r /\ 0 <= r < Z.pos a) ->
(0 < Z.pos a -> Z.pos a < fibonacci (S m)) ->
Zis_gcd (Z.pos a) b
  (Zgcdn n (let (_, r) := Z.div_eucl b (Z.pos a) in r)
     (Z.pos a))
  destruct (Z.div_eucl b (Zpos a)) as (q,r).n:nat
a:positive
b:Z
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
b = Z.pos a * q + r /\ 0 <= r < Z.pos a ->
(0 < Z.pos a -> Z.pos a < fibonacci (S m)) ->
Zis_gcd (Z.pos a) b (Zgcdn n r (Z.pos a))
  intros (->,(H1,H2)) H3.n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 <= r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd (Z.pos a) (Z.pos a * q + r)
  (Zgcdn n r (Z.pos a))
  apply Zis_gcd_for_euclid2.n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 <= r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd r (Z.pos a) (Zgcdn n r (Z.pos a))
  Z.le_elim H1.n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 < r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd r (Z.pos a) (Zgcdn n r (Z.pos a))
n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 = r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd r (Z.pos a) (Zgcdn n r (Z.pos a))
  +n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 < r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd r (Z.pos a) (Zgcdn n r (Z.pos a)) apply Zgcdn_ok_before_fibonacci; auto.n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 < r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
r < fibonacci (S n)
    apply Z.lt_le_trans with (fibonacci (S m));
    [ omega | apply fibonacci_incr; auto].
  +n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q, r:Z
H1:0 = r
H2:r < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd r (Z.pos a) (Zgcdn n r (Z.pos a)) subst r; simpl.n:nat
a:positive
m:nat
Heqm:S m = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S m <= S n)%nat
H0:(1 < S m)%nat
q:Z
H2:0 < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S m)
Zis_gcd 0 (Z.pos a) (Zgcdn n 0 (Z.pos a))
    destruct m as [ |m]; [exfalso; omega| ].n:nat
a:positive
m:nat
Heqm:S (S m) = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S (S m) <= S n)%nat
H0:(1 < S (S m))%nat
q:Z
H2:0 < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S (S m))
Zis_gcd 0 (Z.pos a) (Zgcdn n 0 (Z.pos a))
    destruct n as [ |n]; [exfalso; omega| ].n:nat
a:positive
m:nat
Heqm:S (S m) = (Pos.size_nat a + Pos.size_nat a)%nat
H:(S (S m) <= S (S n))%nat
H0:(1 < S (S m))%nat
q:Z
H2:0 < Z.pos a
H3:0 < Z.pos a -> Z.pos a < fibonacci (S (S m))
Zis_gcd 0 (Z.pos a) (Zgcdn (S n) 0 (Z.pos a))
    simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
 Qed.

 Lemma Zgcdn_is_gcd n a b :
   (Zgcd_bound a <= n)%nat -> Zis_gcd a b (Zgcdn n a b).n:nat
a, b:Z
(Zgcd_bound a <= n)%nat -> Zis_gcd a b (Zgcdn n a b)
 Proof.n:nat
a, b:Z
(Zgcd_bound a <= n)%nat -> Zis_gcd a b (Zgcdn n a b)
   destruct a.n:nat
b:Z
(Zgcd_bound 0 <= n)%nat -> Zis_gcd 0 b (Zgcdn n 0 b)
n:nat
p:positive
b:Z
(Zgcd_bound (Z.pos p) <= n)%nat ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
n:nat
p:positive
b:Z
(Zgcd_bound (Z.neg p) <= n)%nat ->
Zis_gcd (Z.neg p) b (Zgcdn n (Z.neg p) b)
   -n:nat
b:Z
(Zgcd_bound 0 <= n)%nat -> Zis_gcd 0 b (Zgcdn n 0 b) simpl; intros.n:nat
b:Z
H:(1 <= n)%nat
Zis_gcd 0 b (Zgcdn n 0 b)
     destruct n; [exfalso; omega | ].n:nat
b:Z
H:(1 <= S n)%nat
Zis_gcd 0 b (Zgcdn (S n) 0 b)
     simpl; generalize (Zis_gcd_0_abs b); intuition.
   -n:nat
p:positive
b:Z
(Zgcd_bound (Z.pos p) <= n)%nat ->
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b) apply Zgcdn_is_gcd_pos.
   -n:nat
p:positive
b:Z
(Zgcd_bound (Z.neg p) <= n)%nat ->
Zis_gcd (Z.neg p) b (Zgcdn n (Z.neg p) b) rewrite <- Zgcd_bound_opp, <- Zgcdn_opp.n:nat
p:positive
b:Z
(Zgcd_bound (- Z.neg p) <= n)%nat ->
Zis_gcd (Z.neg p) b (Zgcdn n (- Z.neg p) b)
     intros.n:nat
p:positive
b:Z
H:(Zgcd_bound (- Z.neg p) <= n)%nat
Zis_gcd (Z.neg p) b (Zgcdn n (- Z.neg p) b) apply Zis_gcd_minus, Zis_gcd_sym.n:nat
p:positive
b:Z
H:(Zgcd_bound (- Z.neg p) <= n)%nat
Zis_gcd (- Z.neg p) b (Zgcdn n (- Z.neg p) b) simpl Z.opp.n:nat
p:positive
b:Z
H:(Zgcd_bound (- Z.neg p) <= n)%nat
Zis_gcd (Z.pos p) b (Zgcdn n (Z.pos p) b)
     now apply Zgcdn_is_gcd_pos.
 Qed.

 Lemma Zgcd_is_gcd :
   forall a b, Zis_gcd a b (Zgcd_alt a b).forall a b : Z, Zis_gcd a b (Zgcd_alt a b)
 Proof.forall a b : Z, Zis_gcd a b (Zgcd_alt a b)
  unfold Zgcd_alt; intros; apply Zgcdn_is_gcd; auto.
 Qed.