proposition: Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I -> C) : `|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) -> (forall i, P i -> `|F i| = 1) -> {t : C | `|t| == 1 & forall i, P i -> F i = t}.
proof: Proof. case/normC_sum_eq=> t t1 defF normF. by exists t => // i Pi; rewrite defF // normF // mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)