proposition: Lemma subsgroup_in_prop : forall x y : G, in_part x H -> in_part y H -> in_part (sgroup_law _ x y) H.
proof: Proof. intros x y H' H'0; try assumption. apply (subsgroup_prop (G:=G) (s:=H)); auto with algebra. Qed.
imports: Sgroup_facts Parts