proposition: Lemma set_mul1g : left_id [set 1] set_mulg.
proof: Proof. move=> A; apply/setP=> y; apply/imset2P/idP=> [[_ x /set1P-> Ax ->] | Ay]. by rewrite mul1g. by exists (1 : gT) y; rewrite ?(set11, mul1g). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)