Example of a group: ⟨Z,+⟩


Lemma Z_is_CGroup : is_CGroup Z_as_CMonoid Zopp_is_fun.

Definition Z_as_CGroup := Build_CGroup Z_as_CMonoid Zopp_is_fun Z_is_CGroup.

The term Z_as_CGroup is of type CGroup. Hence we have proven that Z is a constructive group.

Canonical Structure Z_as_CGroup.