proposition: Lemma gcd_is_gcd : forall a b : nat, is_gcd a b (gcd a b).
proof: Proof. intros; pattern a, b in |- *; apply gcd_ind; clear a b. intros x; rewrite gcd_def0l; auto. apply is_gcd_Or; auto. intros x; rewrite gcd_def0r; auto. apply is_gcd_Ol; auto. intros a b (H1, (H2, H3)); rewrite <- gcd_def2; split; auto; split; auto. apply divides_plus1; auto. intros d H' H'0. apply H3; auto. apply divides_plus2 with (b := a); auto. rewrite Nat.add_comm; auto. intros a b (H1, (H2, H3)); rewrite <- gcd_def3; split; auto. apply divides_plus1; auto. split; auto. intros d H' H'0. apply H3; auto. apply divides_plus2 with (b := b); auto. rewrite Nat.add_comm; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)