proposition: Lemma nth_mul_mixed a p1 k : nth (mul_mixed tt a p1) k = Rmult a (nth p1 k).
proof: Proof. elim: p1 k => [|x p IHp] k; first by rewrite nth_default // Rmult_0_r. case: k IHp => [|k] IHp //; by rewrite /= IHp. 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