proposition: Lemma nth_default_alt pi p : pi >:: p -> forall n : nat, size pi <= n -> PolR.nth p n = 0%R.
proof: Proof. move=> Hpi n Hn. case: (leqP (PolR.size p) (size pi)) => Hsz. rewrite PolR.nth_default //; exact: leq_trans Hsz Hn. by move/(_ n): Hpi; rewrite nth_default //; move/J.contains_only_0=>->. 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