proposition: Lemma horner_mulCl c p q x : ((mul tt (c :: p) q).[x] = (mul tt p q).[x] * x + c * q.[x])%R.
proof: Proof. rewrite (@hornerE_wide (size p + size q).+1); last by rewrite size_mul leq_pred. have HF : forall i, predT i -> (nth (mul tt (c :: p) q) i.+1 * x ^ i.+1 = (c * nth q i.+1) * x ^ i.+1 + nth (mul tt p q) i * x ^ i.+1)%R. by move=> i; rewrite nth_mulCl Rmult_plus_distr_r. rewrite big_nat_recl // (eq_bigr _ HF). rewrite nth_mul' big_nat1 subn0 [nth _ 0]/= pow_O Rmult_1_r. rewrite (@hornerE_wide (size p + size q)); last by rewrite size_mul leq_pred. set q0 := nth q 0. rewrite (big_endo (fun y => y * x)%R); last 1 [by red=> *; rewrite Rmult_plus_distr_r|by rewrite Rmult_0_l]. rewrite (@hornerE_wide (size p + size q).+1); last by rewrite leqW // leq_addl. rewrite big_nat_recl // pow_O Rmult_1_r; fold q0. rewrite Rmult_plus_distr_l. rewrite (big_endo (fun y => c * y)%R); last 1 [by red=> *; rewrite Rmult_plus_distr_l|by rewrite Rmult_0_r]. rewrite [RHS]Rplus_comm !Rplus_assoc; congr Rplus. rewrite -big_split; apply: eq_bigr => i _. simpl; ring. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec