proposition: Lemma joing_idPr A G : reflect (A <*> G = G) (A \subset G).
proof: Proof. by rewrite joingC; apply: joing_idPl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)