proposition: Lemma gcd_def1 : forall x : nat, gcd x x = x.
proof: Proof. intros x; apply gcd_spec_uniq with (a := x) (b := x); auto. apply gcd_spec_ex3; auto. rewrite Nat.sub_diag; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)