proposition: Theorem Zis_gcd_unique: forall a b c d : Z, Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d).
proof: Proof. intros a b c d [Hc1 Hc2 Hc3] [Hd1 Hd2 Hd3]. assert (c|d) by auto. assert (d|c) by auto. apply Z.divide_antisym; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat