proposition: Lemma normC_sum_eq (I : finType) (P : pred I) (F : I -> C) : `|\sum_(i | P i) F i| = \sum_(i | P i) `|F i| -> {t : C | `|t| == 1 & forall i, P i -> F i = `|F i| * t}.
proof: Proof. have [i /andP[Pi nzFi] | F0] := pickP [pred i | P i & F i != 0]; last first. exists 1 => [|i Pi]; first by rewrite normr1. by case/nandP: (F0 i) => [/negP[]// | /negbNE/eqP->]; rewrite normr0 mul0r. rewrite !(bigD1 i Pi) /= => norm_sumF; pose Q j := P j && (j != i). rewrite -normr_eq0 in nzFi; set c := F i / `|F i|; exists c => [|j Pj]. by rewrite normrM normfV normr_id divff. have [Qj | /nandP[/negP[]// | /negbNE/eqP->]] := boolP (Q j); last first. by rewrite mulrC divfK. have: `|F i + F j| = `|F i| + `|F j|. do [rewrite !(bigD1 j Qj) /=; set z := \sum_(k | _) `|_|] in norm_sumF. apply/eqP; rewrite eq_le ler_normD -(lerD2r z) -addrA -norm_sumF addrA. by rewrite (le_trans (ler_normD _ _)) // lerD2l ler_norm_sum. by case/normCDeq=> k _ [/(canLR (mulKf nzFi)) <-]; rewrite -(mulrC (F i)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)