proposition: Lemma coprime_sqr m n: coprime (m ^2) (n ^ 2) = coprime m n.
proof: Proof. rewrite coprime_pexpr // coprime_pexpl //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)