proposition: Lemma gcd_spec_uniq : forall a b r1 r2 : nat, gcd_spec a b r1 -> gcd_spec a b r2 -> r1 = r2.
proof: Proof. intros a b r1 r2 H'; generalize r2; elim H'; clear H' a b r1 r2. exact gcd_inv_Or. exact gcd_inv_Ol. intros a b c H' H'0 H'1 r2 H'2; inversion H'2; auto. apply H'1; auto. rewrite <- H0; simpl in |- *; rewrite H1; auto. apply H'1; auto. rewrite <- H; simpl in |- *; rewrite Nat.sub_0_r; rewrite H1; auto. contradict H; auto with arith. intros a b c H' H'0 H'1 r2 H'2; inversion H'2; auto. apply H'1; auto. rewrite <- H0; simpl in |- *; rewrite H1; rewrite Nat.sub_0_r; auto. apply H'1; auto. rewrite <- H; simpl in |- *; rewrite H1; auto. contradict H; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)