proposition: Lemma conjgK : @right_loop T T invg conjg.
proof: Proof. by move=> y x; rewrite -conjgM mulgV conjg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)