What would be a more convenient better way to solve this proof in a less clustered/confusing way?
Lemma trial_ex : forall a b c d : Z, (a | b * c) -> Zis_gcd a b d -> (a | c * d).
Proof.
intros a b c d H1 H2.
destruct H1 as [z H3].
exists (d * z).
apply Zis_gcd_bezout in H2.
destruct H2 as [x y H4].
unfold Z.divide in *.
destruct H3 as [H5 H6].
rewrite <- H4.
rewrite Z.mul_add_distr_r.
rewrite H4.
replace (x * (a * z)) with (x * a * z) by ring.
replace (y * b * z) with (y * (b * z)) by ring.
replace (x * a * z + y * (b * z)) with (x * a * z + y * b * z) by ring.
replace (x * a * z + y * b * z) with ((x * a + y * b) * z) by ring.
replace (x * a + y * b) with d by assumption.
rewrite <- H4.
rewrite <- Z.mul_add_distr_r.
rewrite Z.mul_comm with (n:=a) (m:=c).
rewrite Z.mul_assoc.
reflexivity.
d * c = d * (b * c)
. I think you will have to take into account the mathematical intuition of this lemma, before translating its proof into Coq. $\endgroup$