proposition: Lemma mul1q: left_id one mul.
proof: Proof. by move=> x; rewrite -[x]reprK !piE mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)