proposition: Lemma Z_is_CGroup : is_CGroup Z_as_CMonoid Zopp_is_fun.
proof: Proof. red in |- *. simpl in |- *. intro x. split; simpl in |- *. apply Zplus_opp_r. apply Zplus_opp_l. Qed.
imports: CoRN.model.monoids.Zmonoid CoRN.algebra.CGroups