CoRN.model.groups.Qposgroup

Require Export Qposmonoid.
Require Export CGroups.

Example of a group: ⟨Qpos,[*]⟩

The positive rational numbers form a multiplicative group.

Lemma Qpos_is_CGroup : is_CGroup Qpos_mult_as_CMonoid Qpos_inv_op.
Proof.
intros x.
split; simpl; autorewrite with QposElim; field; apply Qpos_nonzero.
Qed.

Definition Qpos_as_CGroup := Build_CGroup
Qpos_mult_as_CMonoid Qpos_inv_op Qpos_is_CGroup.