proposition: Lemma PS_is_CGroup : forall A : CSetoid, is_CGroup (PS_as_CMonoid A) (Inv_as_un_op A).
proof: Proof. intro A. unfold is_CGroup in |- *. intro x. unfold is_inverse in |- *. simpl in |- *. split. case x. simpl in |- *. intros f H. unfold eq_fun in |- *. intro a. unfold comp in |- *. simpl in |- *. apply inv2. case x. simpl in |- *. intros f H. unfold eq_fun in |- *. intro a. unfold comp in |- *. simpl in |- *. apply inv1. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids