proposition: Lemma conjg_inj : @left_injective T T T conjg.
proof: Proof. by move=> y; apply: can_inj (conjgK y). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)