proposition: Lemma normr_sumprod f g n : `| \sum_(i< n) (f i * g i) | <= (\max_(i< n) `|f i|) * \sum_ (i<n) `| g i|.
proof: Proof. apply: le_trans (_: \sum_(i < n) `| f i * g i| <= _). apply: ler_norm_sum. have ->: \sum_(i < n) `|f i * g i| = \sum_(i < n) `|f i| * `|g i|. by apply: eq_big => // i; rewrite normrM. rewrite mulr_sumr; apply: ler_sum => i _; apply: ler_wpmul2r. by rewrite normr_ge0. by apply: (bigmaxf_le (fun i => `|f i|)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)