CoRN.model.abgroups.CRabgroup

Require Export CRgroup.
Require Import CRcorrect.
Require Export CAbGroups.
Require Import CornTac.

Example of a abelian group: ⟨CR,+⟩

Open Local Scope uc_scope.

Lemma CRisCAbGroup : is_CAbGroup CRasCGroup.
Proof.
intros x y.
change (x+y==y+x)%CR.
rewrite <- CR_eq_as_Cauchy_IR_eq.
stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR y)); [| now apply CR_plus_as_Cauchy_IR_plus].
stepr ((CRasCauchy_IR y)[+](CRasCauchy_IR x)); [| now apply CR_plus_as_Cauchy_IR_plus].
apply cag_commutes.
Qed.

Definition CRasCAbGroup : CAbGroup :=
Build_CAbGroup _ CRisCAbGroup.

Canonical Structure CRasCAbGroup.