proposition: Lemma gcd_ex : forall a b : nat, {r : nat | gcd_spec a b r}.
proof: Proof. intros a b; pattern b, a in |- *; apply gcd_rec; clear a b. intros a; exists a; auto. intros b; exists b; auto. intros a b Rr; case Rr; intros r Hr; exists r. apply gcd_spec_ex3; auto with arith. rewrite Nat.add_sub; auto; rewrite Nat.sub_diag; auto. intros a b Rr; case Rr; intros r Hr; exists r. case (zerop a); intros lta. rewrite lta; simpl in |- *. rewrite <- (gcd_inv_Or b r); auto. apply gcd_spec_ex3; auto with arith. rewrite Nat.sub_diag; auto. rewrite <- lta; auto. apply gcd_spec_ex2; auto with arith. pattern b at 1 in |- *; replace b with (0 + b); auto with arith. rewrite Nat.add_sub; auto; rewrite Nat.sub_diag; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)