proposition: Lemma subgroup_in_prop : forall x : G, in_part x H -> in_part (group_inverse _ x) H.
proof: Proof. intros x H'; try assumption. apply (subgroup_prop (G:=G) (s:=H)); auto with algebra. Qed.
imports: Sub_monoid Group_facts