proposition: Lemma Zis_gcd_0_abs a : Zis_gcd 0 a (Z.abs a).
proof: Proof. apply Zabs_ind. - intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. - intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat