proposition: Lemma Zgcd_mod_lft : forall a b : Z, (b > 0)%Z -> Zgcd (a mod b) b = Zgcd a b.
proof: Proof. intros a b Hb. replace (a mod b)%Z with (a - b * (a / b))%Z. apply Zgcd_minus_elim_lr. apply Zdivides_mult_elim_rht. apply Zdivides_ref. generalize (Z_div_mod_eq_full a b). auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)