proposition: Lemma mul_mixed_correct u ai pi a p : ai >: a -> pi >:: p -> mul_mixed u ai pi >:: PolR.mul_mixed tt a p.
proof: Proof. move=> Ha Hp; rewrite /mul_mixed /PolR.mul_mixed. apply: (seq_foldr_correct (Rel := fun v t => t >: v)) =>//. - move=> x s /J.contains_only_0 -> Hs [|k] /=; first by rewrite Rmult_0_r; apply: J.zero_correct. by move: (Hs k); rewrite nth_nil. - move=> x s Hx Hs [|k]; first by rewrite -(Rmult_0_r a); apply: J.mul_correct. by move: (Hs k); rewrite nth_nil. - move=> x y s t Hx Hs [|k]; first by apply: J.mul_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