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