proposition: Lemma biv_horner_seqopP (n k : int) (biv_cf0 : int -> int -> R := fun _ _ => 0) : biv_horner_seqop n k = \sum_(0 <= j < size cf) nth biv_cf0 cf j n k * u (int.shift j n) k.
proof: Proof. rewrite -[LHS]/(horner_seqop [seq a ^~ k | a <- cf] (u ^~ k) n). rewrite horner_seqopP size_map [LHS]big_seq_cond [RHS]big_seq_cond. apply: eq_bigr=> i /andP []; rewrite mem_index_iota=> /andP [_ hi] _. by rewrite (nth_map biv_cf0). Qed.
imports: mathcomp(all_ssreflect all_algebra) shift bigopz