CoRN.model.groups.QSposgroup

Require Export QSposmonoid.
Require Import CGroups.

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

The positive rationals form with the operation (x,y) ↦ xy/2 a CGroup.

Lemma Qpos_multdiv2_is_CGroup : is_CGroup Qpos_multdiv2_as_CMonoid divmult4.
Proof.
intro x.
unfold is_inverse.
split; simpl; field; auto with ×.
Qed.

Definition Qpos_multdiv2_as_CGroup := Build_CGroup
Qpos_multdiv2_as_CMonoid divmult4 Qpos_multdiv2_is_CGroup.