proposition: Lemma size_dotmuldiv (n : nat) (u : U) a b p : size p = n -> seq.size a = n -> seq.size b = n -> size (dotmuldiv u a b p) = n.
proof: Proof. move: a b p n; elim=> [|a0 a1 IH] [|b0 b1] [|p0 p1] =>//. move=> /= n Hp Ha Hb /=. rewrite (IH _ _ n.-1) //. by rewrite -Hp. by rewrite -Hp. by rewrite -Ha. by rewrite -Hb. 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