proposition: Theorem Zis_gcd_uniqueness_apart_sign : forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'.
proof: Proof. intros a b d d'; simple induction 1. intros H1 H2 H3; destruct 1 as [H4 H5 H6]. generalize (H3 d' H4 H5); intro Hd'd. generalize (H6 d H1 H2); intro Hdd'. exact (Z.divide_antisym d d' Hdd' Hd'd). Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat