proposition: Lemma ler_norm_sum I r (G : I -> V) (P : pred I): `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i|.
proof: Proof. elim/big_rec2: _ => [|i y x _]; first by rewrite normr0. by rewrite -(lerD2l `|G i|); apply: le_trans; apply: ler_normD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)