proposition: Lemma Zrelprime_gcd_mult_elim_rht : forall a b c : Z, Zrelprime a b -> Zgcd c (a * b) = (Zgcd c a * Zgcd c b)%Z.
proof: Proof. intros a b c; rewrite (Zgcd_symm c (a * b)); rewrite (Zgcd_symm c a); rewrite (Zgcd_symm c b); apply Zrelprime_gcd_mult_elim_lft. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)