proposition: Lemma totient_coprime m n : coprime m n -> totient (m * n) = totient m * totient n.
proof: Proof. move=> co_mn; have [-> //| m_gt0] := posnP m. have [->|n_gt0] := posnP n; first by rewrite !muln0. rewrite !totientE ?muln_gt0 ?m_gt0 //. have /(perm_big _)->: perm_eq (primes (m * n)) (primes m ++ primes n). apply: uniq_perm => [||p]; first exact: primes_uniq. by rewrite cat_uniq !primes_uniq -coprime_has_primes // co_mn. by rewrite mem_cat primesM. rewrite big_cat /= !big_seq. congr (_ * _); apply: eq_bigr => p; rewrite mem_primes => /and3P[_ _ dvp]. rewrite (mulnC m) logn_Gauss //; move: co_mn. by rewrite -(divnK dvp) coprimeMl => /andP[]. rewrite logn_Gauss //; move: co_mn. by rewrite coprime_sym -(divnK dvp) coprimeMl => /andP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)