proposition: Lemma expfzMl x y n : (x * y) ^ n = x ^ n * y ^ n.
proof: Proof. have [->|/negPf n0] := eqVneq n 0; first by rewrite !expr0z mulr1. case: (boolP ((x * y) == 0)); rewrite ?mulf_eq0. by case/pred2P=> ->; rewrite ?(mul0r, mulr0, exp0rz, n0). by case/norP=> x0 y0; rewrite exprzMl ?unitfE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)