proposition: Lemma nth_opp p1 k : nth (opp p1) k = Ropp (nth p1 k).
proof: Proof. rewrite /nth /add nth_map_dflt -!/(nth _ _). by case: (leqP (size p1) k) => H1; rewrite ?(nth_default H1); 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