proposition: Lemma mulq_addl: left_distributive mul +%R.
proof: Proof. move=> x y z; rewrite -[x]reprK -[y]reprK -[z]reprK. by apply/eqP; rewrite piE /= mulrDl equiv_refl. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)