CoRN.model.groups.CRgroup

Require Export CRGroupOps.
Require Export CRmonoid.
Require Import CRcorrect.
Require Import CornTac.

Open Local Scope uc_scope.

Lemma CRopp_strext : un_op_strext CRasCSetoid CRopp.
Proof.
 intros x y H.
 change (CRapartT x y)%CR.
 apply CR_ap_as_Cauchy_IR_ap_2.
 apply: un_op_strext_unfolded.
 stepl (CRasCauchy_IR (-x)%CR); [| now apply eq_symmetric; apply CR_opp_as_Cauchy_IR_opp].
 stepr (CRasCauchy_IR (-y)%CR); [| now apply eq_symmetric; apply CR_opp_as_Cauchy_IR_opp].
 apply CR_ap_as_Cauchy_IR_ap_1.
 apply H.
Qed.

Definition CRoppasUnOp : CSetoid_un_op CRasCSetoid :=
Build_CSetoid_fun _ _ _ CRopp_strext.

Lemma CRisCGroup : is_CGroup CRasCMonoid CRoppasUnOp.
Proof.
 split.
  change (x-x==0)%CR.
  rewrite <- CR_eq_as_Cauchy_IR_eq.
  stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR (- x)%CR)); [| now apply CR_plus_as_Cauchy_IR_plus].
  stepl ((CRasCauchy_IR x)[+][--](CRasCauchy_IR x)); [| now
    apply plus_resp_eq; apply CR_opp_as_Cauchy_IR_opp].
  apply: eq_transitive.
   apply cg_rht_inv_unfolded.
  apply: CR_inject_Q_as_Cauchy_IR_inject_Q.
 change (-x + x==0)%CR.
 rewrite <- CR_eq_as_Cauchy_IR_eq.
 stepl ((CRasCauchy_IR (-x)%CR)[+](CRasCauchy_IR x)); [| now apply CR_plus_as_Cauchy_IR_plus].
 stepl ([--](CRasCauchy_IR x)[+](CRasCauchy_IR x)); [| now
   apply bin_op_is_wd_un_op_lft; apply CR_opp_as_Cauchy_IR_opp].
 apply: eq_transitive.
  apply cg_lft_inv_unfolded.
 apply: CR_inject_Q_as_Cauchy_IR_inject_Q.
Qed.

Definition CRasCGroup : CGroup :=
Build_CGroup _ _ CRisCGroup.

Canonical Structure CRasCGroup.