proposition: Lemma Zgcd_mod0_lft : forall a b : Z, Zgcd a b <> 0%Z -> (a mod Zgcd a b)%Z = 0%Z.
proof: Proof. intros; apply Zmod0_Zdivides; auto; apply Zgcd_is_divisor_lft. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)