Here are some proposed formal definitions in group theory for group, subgroup and left cosets for use in a computerized, formal system. Do they conform to the standard definitions? Online notes seem a bit vague for my purposes. I want to be sure I have captured the essence of these concepts before proceeding with my project.
Group
$\forall G,*: [Group(G,*) \iff \forall a,b\in G: a*b\in G$
$\land \forall a,b,c\in G: (a*b)*c=a*(b*c)$
$\land \exists e\in G: [\forall x\in G: [e*x=x \land x*e=x]$
$\land \forall a \in G: \exists b\in G: [b*a=e \land a*b=e]]]$
Subgroup $H\le G$
$\forall G, H, *:[Group(G,*) \implies [H\le G \iff Group(H,*) \land H\subseteq G]]$
Left Coset $L(a,H,G,*,x)$
$\forall G, H, *, x: [Group(G,*)\land H\le G \land x\in G$
$ \implies \forall a: L(a,H,G,*,x) \iff \forall b:[b\in a \iff \exists c\in H: b=x*c]]$
where $L(a,H,G,*,x)$ means $a$ is the left coset of $H$ in $G$ wrt $x$.
EDIT: Would the following definitions for subgroup and left coset also work?
$\forall G, H, *:[Group(G,*) \land Group(H,*) \implies [H\le G \iff H\subseteq G]]$
$\forall G, H, *, x: [Group(G,*)\land Group(H,*) \land H\le G \land x\in G$
$ \implies \forall a: L(a,H,G,*,x) \iff \forall b:[b\in a \iff \exists c\in H: b=x*c]]$