proposition: Lemma biv_horner_seqop2P (n k : int) (biv_cf0 : int -> int -> R := fun _ _ => 0) : biv_horner_seqop2 u n k = \sum_(0 <= i < size cf) \sum_(0 <= j < size (nth [::] cf i)) nth biv_cf0 (nth [::] cf i) j n k * u (int.shift j n) (int.shift i k).
proof: Proof. rewrite /biv_horner_seqop2; elim: cf u => [ | cf0 c ihc] u'. by rewrite /= big_nil. by rewrite /= {}ihc biv_horner_seqopP /= big_nat_recl //= addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) shift bigopz