proposition: Lemma gcd_aux x y (g := gcdn x y) (x' := x%/g) (y':= y%/ g): 0 < x -> [/\ x = x' * gcdn x y, y = y' * gcdn x y & coprime x' y'].
proof: Proof. move => xp. case: (egcdnP y xp) => u v /= /eqP bz _. move: (dvdn_gcdl x y)(dvdn_gcdr x y); rewrite !dvdn_eq => /eqP xv /eqP yv. split =>//. move: bz; rewrite -[gcdn x y]mul1n -{1} yv -{1} xv !mulnA -mulnDl addnC. by rewrite eqn_pmul2r ?gcdn_gt0 ?xp // addnC => /eqP /coprime_if_bezout. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)