proposition: Lemma comp_polyM p q r : (p * q) \Po r = (p \Po r) * (q \Po r).
proof: Proof. exact: rmorphM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)