CoRN.model.monoids.QSposmonoid

Require Export QSpossemigroup.
Require Import CMonoids.

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

Two is the unit of the operation (x,y) ↦ xy/2 on the positive rationals. So we have another monoid structure on the positive rational numbers.

Lemma QTWOpos_is_rht_unit : is_rht_unit multdiv2 (2%positive:Qpos).
Proof.
intros x.
simpl.
autorewrite with QposElim.
field.
Qed.

Lemma QTWOpos_is_lft_unit : is_lft_unit multdiv2 (2%positive:Qpos).
Proof.
intros x.
simpl.
autorewrite with QposElim.
field.
Qed.

Definition Qpos_multdiv2_is_CMonoid := Build_is_CMonoid
Qpos_multdiv2_as_CSemiGroup _ QTWOpos_is_rht_unit QTWOpos_is_lft_unit.

Definition Qpos_multdiv2_as_CMonoid := Build_CMonoid
Qpos_multdiv2_as_CSemiGroup _ Qpos_multdiv2_is_CMonoid.