proposition: Lemma Qpos_is_CGroup : is_CGroup Qpos_mult_as_CMonoid Qpos_inv_op.
proof: Proof. intros x. split; simpl; autorewrite with QposElim; field; apply Qpos_nonzero. Qed.
imports: CoRN.model.monoids.Qposmonoid CoRN.algebra.CGroups