proposition: Lemma conjJg x y z : (x ^ y) ^ z = (x ^ z) ^ y ^ z.
proof: Proof. by rewrite 2!conjMg conjVg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)