proposition: Lemma horner_seqopP cf u n (cf0 := fun _ => 0) : horner_seqop cf u n = \sum_(0 <= i < size cf) nth cf0 cf i n * u (int.shift i n).
proof: Proof. rewrite /horner_seqop; elim: cf {1 4}n => [ | a cf' ihcf] m. by rewrite big_mkord big_ord0. case: cf' ihcf => [_ /= | b cf' ihcf]. by rewrite big_mkord big_ord1 /=. have -> : horner_seqop_rec [:: a, b & cf'] u m n = (horner_seqop_rec [::b & cf'] u (int.shift 1%N m) n) + a n * u m by []. symmetry; rewrite ihcf [size _]/= big_nat_recl // addrC; congr (_ + _). apply: eq_bigr=> i _; congr (_ * _); rewrite !int.zshiftP -addn1 PoszD addrAC. by rewrite addrA. Qed.
imports: mathcomp(all_ssreflect all_algebra) shift bigopz