CoRN.model.abgroups.QSposabgroup


Require Export QSposgroup.
Require Import CAbGroups.

Example of an abelian group: ⟨Qpos, (x,y) ↦ xy/2⟩

The positive rational numbers form with the operation (x,y) ↦ xy/2 an abelian group.

Lemma Qpos_multdiv2_is_CAbGroup : is_CAbGroup Qpos_multdiv2_as_CGroup.
Proof.
 intros x y.
 simpl.
 QposRing.
Qed.

Definition Qpos_multdiv2_as_CAbGroup := Build_CAbGroup
 Qpos_multdiv2_as_CGroup Qpos_multdiv2_is_CAbGroup.