proposition: Lemma nth_primitive (p : T) (c : R) (k : nat) : nth (primitive tt c p) k = if size p < k then 0%R else int_coeff tt p c k.
proof: Proof. case: ifP => Hk. by rewrite nth_default // size_primitive. case : k Hk => [ _ | m Hm] //=. have HSiota : m < seq.size (iota 0 (size p)). by rewrite size_iota; rewrite ltnNge in Hm; move/negbFE in Hm. rewrite /nth /toSeq /primitive /= . rewrite (nth_map 0) // nth_iota; first by rewrite add0n. by rewrite ltnNge in Hm; move/negbFE in Hm. 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