CoRN.model.abgroups.Qposabgroup

Require Export Qposgroup.
Require Import CAbGroups.

Example of an abelian group: ⟨Qpos,[*]⟩

The positive rationals form with the multiplication a CAbgroup.

Definition Qpos_mult_is_CAbGroup : is_CAbGroup Qpos_as_CGroup.
Proof.
intros x y; simpl.
QposRing.
Qed.

Definition Qpos_mult_as_CAbGroup := Build_CAbGroup
Qpos_as_CGroup Qpos_mult_is_CAbGroup.