proposition: Lemma Zp_mul_addl : left_distributive Zp_mul Zp_add.
proof: Proof. by move=> x y z; rewrite -!(Zp_mulC z) Zp_mul_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)