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