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