proposition: Lemma unit_mul1u : left_id unit1 unit_mul.
proof: Proof. by move=> u; apply/val_inj/mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)