fact: Record subsgroup : Type := {subsgroup_part : Predicate G; subsgroup_prop : forall x y : G, in_part x subsgroup_part -> in_part y subsgroup_part -> in_part (sgroup_law _ x y) subsgroup_part}.
imports: Sgroup_facts Parts