proposition: Lemma polyCons_correct pi xi p x : pi >:: p -> xi >: x -> polyCons xi pi >:: PolR.polyCons x p.
proof: Proof. by move=> Hp Hx [|k] /=. 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