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.