# Organizing a Coq proof

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 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_comm with (n:=a) (m:=c).
rewrite Z.mul_assoc.
reflexivity.

• Welcome to PA.SE! This is a good question. It is okay to set up multiple accounts, as long as you don't use them to vote oneself, circumvent bans, etc. I'm not an expert of Coq, but I hope someone else can answer your question!
– Trebor
May 17 at 2:56
• Did you try to write a draft proof with pen and paper? Your proof script did not compile on my computer (V 8.16). I don't think its OK to send snippets with errors. About readability: while and after building a proof, using bullets, tacticals, regrouping rewrites may help a lot. May 17 at 6:52
• A last comment about your proof. The third line leads to a state where you would have to prove 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. May 17 at 8:47
• You should provide a MWE (stackoverflow.com/help/minimal-reproducible-example), so people can help you. Although the terms permit, I encourage you to register an account and build your reputation in the community. Even just asking interesting questions is a good way to build reputation. May 17 at 23:10

Indeed, in your tentative proof, you made a classic mistake: using the existential quantifier introduction tactic too early (i.e. without a sufficient context).

In the script below, I use Zis_gcd_bezoutto get uand v, which are used in the argument of the exists tactic.

Require Import ZArith.
Open Scope Z_scope.
Require Import Znumtheory.

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].
apply Zis_gcd_bezout in H2; destruct H2 as [u v Huv].
exists (c * u + v * z).
(* now easy to complete ...  *)

• if only eexists would work here...
– cody
Jun 29 at 19:50