CoRN.model.monoids.Qposmonoid

Require Export Qpossemigroup.
Require Import CMonoids.

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

One is the unit for multiplication on positive integers. Therefore the positive rational numbers together with the multiplication are a CMonoid.

Lemma QONEpos_is_rht_unit : is_rht_unit Qpos_mult_is_bin_fun (1%positive:Qpos).
Proof.
intros x.
simpl.
ring.
Qed.

Lemma QONEpos_is_lft_unit : is_lft_unit Qpos_mult_is_bin_fun (1%positive:Qpos).
Proof.
intros x.
simpl.
ring.
Qed.

Definition Qpos_mult_is_CMonoid := Build_is_CMonoid
Qpos_mult_as_CSemiGroup _ QONEpos_is_rht_unit QONEpos_is_lft_unit.

Definition Qpos_mult_as_CMonoid := Build_CMonoid
Qpos_mult_as_CSemiGroup _ Qpos_mult_is_CMonoid.