Recall our definition of groups in Coq from the last time:

```
Structure group :=
{
G :> Set;
id : G;
op : G -> G -> G;
inv : G -> G;
op_assoc : forall (x y z : G), op x (op y z) = op (op x y) z;
op_inv_l : forall (x : G), id = op (inv x) x;
op_id_l : forall (x : G), x = op id x
}.
```

This is a record. You can construct a value of type `group`

by providing a value
for all the fields. By default, the constructor is called `Build_group`

:

```
Build_group
: forall (G : Set) (id : G) (op : G -> G -> G) (inv : G -> G),
(forall x y z : G, op x (op y z) = op (op x y) z) ->
(forall x : G, op (inv x) x = id) ->
(forall x : G, op id x = x) -> group
```

This is also the reason why we didn’t include the right-hand side versions of
`op_inv_l`

and `op_id_l`

into the definition of `group`

. If we did, you’d have
to provide proofs of the right-hand side laws when constructing a `group`

value.

We can construct the trivial group over `unit`

:

```
Example trivial_group : group.
refine (Build_group unit tt (fun _ _ => tt) (fun _ => tt) _ _ _).
- intros. auto.
- intros. auto.
- intros. destruct x. trivial.
Defined.
```

More interestingly, we can define the additive group of integers `Z`

. Since
Coq’s standard library contains a good set of properties for `Z`

, defining the
group is straightforward.

```
Require Import Coq.ZArith.BinInt.
Open Scope Z.
Example Z_add_group : group.
refine (Build_group Z (0 : Z) Z.add Z.opp Z.add_assoc Z.add_opp_diag_l _).
- trivial.
Defined.
```