proposition: Lemma nth_div_mixed_r p1 b k : nth (div_mixed_r tt p1 b) k = Rdiv (nth p1 k) b.
proof: Proof. elim: p1 k => [|x p IHp] k; first by rewrite nth_default // /Rdiv Rmult_0_l. case: k IHp => [|k] IHp //; by rewrite /= IHp. 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