proposition: Lemma Zgcd_mod_rht : forall a b : Z, (a > 0)%Z -> Zgcd a (b mod a) = Zgcd a b.
proof: Proof. intros a b Ha. repeat rewrite (Zgcd_symm a); apply Zgcd_mod_lft; exact Ha. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)