proposition: Lemma dotmuldiv_propagate u a b p : seq.size a = size p -> seq.size b = size p -> poly_eqNai p -> poly_eqNai (dotmuldiv u a b p).
proof: Proof. move=> Ha Hb Hp; red => k Hk. rewrite (@size_dotmuldiv (size p)) // in Hk. rewrite nth_dotmuldiv Ha Hb !orbb ifF. rewrite I.mul_propagate_r //. exact: Hp. by rewrite leqNgt Hk. 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