$7$ Divisibility and GCD

Prove that

$$abc in Z$,($a$|$c$)=($b$|$c$)=1=$gcd$($a$,$b$)=($ab$|$c$).$

following the instructions for an acceptable proof. The Coq statement is

Lemma prob$7$ : forall a b c : Z$,($a $|$ c$)->($b $|$ c$)->$ Zis$\_$gcd a b $1->($a$*$b $|$ c$).$ The Zis gcd bezout lemma can be apply$$ed to get a Bezout statement, which

can then be destructed, to get the Bezout relation from Zis gcd$.$

Use the template:

Open Scope Z$\_$scope.

Require Import ZArith.

Require Import Znumtheory.

Lemma prob$7$ : forall a b c : Z$,($a $|$ c$)->($b $|$ c$)->$ Zis$\_$gcd a b $1->($a$*$b $|$ c$).$

Proof.

Qed.