proposition: Lemma conjg_fixP x y : reflect (x ^ y = x) ([~ x, y] == 1 :> T).
proof: Proof. by rewrite -eq_mulVg1 eq_sym; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)