proposition: Lemma Qpos_multdiv2_is_CGroup : is_CGroup Qpos_multdiv2_as_CMonoid divmult4.
proof: Proof. intro x. unfold is_inverse. split; simpl; field; auto with *. Qed.
imports: CoRN.model.monoids.QSposmonoid CoRN.algebra.CGroups