proposition: Lemma factor_square a b c (u:=a %/ gcdn a c) (v := c %/ gcdn a c): 0 < a -> coprime a b -> a * b = c ^2 -> [/\ a = u ^2, b = v^2 & coprime u v].
proof: Proof. move => ap cab /eqP Eq. move:(gcd_aux c ap); rewrite -/u -/v; move => [av cv cuv]. move: cab; rewrite av coprimeMl => /andP [cub cgb]. move: Eq; rewrite {1}av {2} cv mulnAC expnMn - (mulnn (gcdn a c)) mulnA. rewrite eqn_pmul2r ?gcdn_gt0 ? ap // => /eqP Eq. move:ap; rewrite {1}av muln_gt0 => /andP [up _]. have: (u %| v ^ 2 * gcdn a c) by rewrite -Eq /dvdn modnMr. have: (gcdn a c %| b * u ) by rewrite mulnC Eq /dvdn mulnC modnMr. rewrite !Gauss_dvdr ? coprimeXr // => dvd1 dvd2. move: (eqn_dvd (gcdn a c) u); rewrite dvd1 dvd2 /= => /eqP gv. by move /eqP:Eq; rewrite gv mulnn mulnC eqn_pmul2r // => /eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)