fact: Parameter size_mul_tail : forall u n p q, size (mul_tail u n p q) = ((size p) + (size q)).-1 - n.+1.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec