proposition: Lemma is_gcd_unic : forall a b c d : nat, is_gcd a b c -> is_gcd a b d -> c = d.
proof: Proof. intros a b c d (H1, (H2, H3)) (H5, (H6, H7)). apply divides_antisym; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)