proposition: Lemma groupD1_inj G H : G^# = H^# -> G :=: H.
proof: Proof. by move/(congr1 (setU 1)); rewrite !setD1K. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)