CoRN.model.groups.Qgroup

Require Export Qmonoid.
Require Import CGroups.

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.
Proof. split. apply Qplus_opp_r. simpl. rewrite Qplus_comm. apply Qplus_opp_r. Qed.

Definition Q_as_CGroup := Build_CGroup Q_as_CMonoid Qopp_is_fun Q_is_CGroup.

Canonical Structure Q_as_CGroup.