proposition: Lemma size_mul_eq1 p q : (size (p * q) == 1) = ((size p == 1) && (size q == 1)).
proof: Proof. have [->|pNZ] := eqVneq p 0; first by rewrite mul0r size_poly0. have [->|qNZ] := eqVneq q 0; first by rewrite mulr0 size_poly0 andbF. rewrite size_mul //. by move: pNZ qNZ; rewrite -!size_poly_gt0; (do 2 case: size) => //= n [|[|]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)