proposition: Lemma normr_sumprod1 f g n b: 0 <= b -> (forall i, (i<n)%N -> `|f i| <= b) -> `| \sum_(i< n) (f i * g i) | <= b * \sum_ (i<n) `| g i|.
proof: Proof. move=> b0 h; apply: (le_trans (normr_sumprod f g n)). apply: ler_wpmul2r; first by rewrite sumr_ge0 // => i _; rewrite absr_ge0. exact /(bigmaxf_lerP (fun z => `|f z|) n b0). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)