proposition: Lemma mulrBl x y z : (y - z) * x = y * x - z * x.
proof: Proof. by rewrite mulrDl mulNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)