proposition: Lemma gcd_def3 : forall a b : nat, gcd a b = gcd (a + b) b.
proof: Proof. intros a b; apply gcd_spec_uniq with (a := a + b) (b := b); auto. case (zerop a); intros lta. rewrite lta; simpl in |- *; rewrite gcd_def0l; auto. apply gcd_spec_ex3; auto with arith. rewrite Nat.sub_diag; auto. apply gcd_spec_ex3; auto with arith. rewrite Nat.add_sub. apply gcd_correct; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)