proposition: Lemma mulz_addl : left_distributive mulz (+%R).
proof: Proof. move=> x y z; elim: z=> [|n|n]; first by rewrite !(mul0z,mulzC). by rewrite !mulzS=> ->; rewrite !addrA [X in X + _]addrAC. rewrite !mulzN !mulzS -!opprD=> /oppr_inj->. by rewrite !addrA [X in X + _]addrAC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)