proposition: Lemma invg_lcosets A B : (lcosets A B)^-1 = rcosets A^-1 B^-1.
proof: Proof. rewrite /A^-1/= -![_^-1](can_imset_pre _ invgK) -[RHS]imset_comp -imset_comp. by apply: eq_imset => x /=; rewrite lcosetE rcosetE invMg invg_set1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)