proposition: Lemma Zgcd_div_mult_rht : forall a b : Z, Zgcd a b <> 0%Z -> b = (b / Zgcd a b * Zgcd a b)%Z.
proof: Proof. intros a b. rewrite Zgcd_symm. apply Zgcd_div_mult_lft. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)