proposition: Lemma set_invgM : {morph set_invg : A B / set_mulg A B >-> set_mulg B A}.
proof: Proof. move=> A B; apply/setP=> z; rewrite inE. apply/imset2P/imset2P=> [[x y Ax By /(canRL invgK)->] | [y x]]. by exists y^-1 x^-1; rewrite ?invMg // inE invgK. by rewrite !inE => By1 Ax1 ->; exists x^-1 y^-1; rewrite ?invMg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)