proposition: Lemma div_mixed_r_correct u pi bi p b : pi >:: p -> bi >: b -> div_mixed_r u pi bi >:: PolR.div_mixed_r tt p b.
proof: Proof. move=> Ha Hp; rewrite /div_mixed_r /PolR.div_mixed_r. apply: (seq_foldr_correct (Rel := fun v t => t >: v)) =>//. - move=> x s /J.contains_only_0 -> Hs [|k] /=; first by rewrite /Rdiv Rmult_0_l; apply: J.zero_correct. by move: (Hs k); rewrite nth_nil. - move=> x s Hx Hs [|k]; last by move: (Hs k); rewrite nth_nil. by rewrite -(Rmult_0_l (Rinv b)); apply: J.div_correct. - move=> x y s t Hx Hs [|k]; first by apply: J.div_correct. by apply: Hs. 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