Example of a group: ⟨Q,+⟩

The rational numbers with addition form a group. The inverse function is taking the opposite.

Lemma Q_is_CGroup : is_CGroup Q_as_CMonoid Qopp_is_fun.

Definition Q_as_CGroup := Build_CGroup Q_as_CMonoid Qopp_is_fun Q_is_CGroup.

Canonical Structure Q_as_CGroup.