proposition: Lemma nth_add p1 p2 k : nth (add tt p1 p2) k = Rplus (nth p1 k) (nth p2 k).
proof: Proof. rewrite /nth /add nth_map2_dflt -!/(nth _ _). by case: (leqP (size p1) k) => H1; case: (leqP (size p2) k) => H2; rewrite ?(nth_default H1) ?(nth_default H2); auto with real. 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