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