proposition: Lemma Zgcd_mult_elim_ll : forall a b : Z, Zgcd (b * a) a = Z.abs a.
proof: Proof. intros a b. elim (Zdec (b * a)). intro Hab; rewrite Hab; rewrite Zgcd_zero_lft; reflexivity. intro Hab; apply Zgcd_divisor; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)