proposition: Lemma normr_sum : forall m (G : nat -> F), `|\sum_(i < m) G i| <= \sum_(i < m) `|G i|.
proof: Proof. elim=> [|m ihm] G; first by rewrite !big_ord0 normr0. rewrite !big_ord_recr /=; apply: le_trans (ler_norm_add _ _) _=> /=. by rewrite ler_add2r; apply: ihm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc