proposition: Lemma cag_commutes_unfolded : forall x y : G, x[+]y [=] y[+]x.
proof: Proof. Proof cag_commutes. End AbGroup_Axioms. Section SubCAbGroups. Variable G : CAbGroup. Variable P : G -> CProp. Variable Punit : P [0]. Variable op_pres_P : bin_op_pres_pred _ P csg_op. Variable inv_pres_P : un_op_pres_pred _ P cg_inv. Let subcrr : CGroup := Build_SubCGroup _ _ Punit op_pres_P inv_pres_P. Lemma isabgrp_scrr : is_CAbGroup subcrr. Proof. red in |- *. intros x y. case x. case y. intros. simpl in |- *. apply cag_commutes_unfolded. Qed.
imports: CoRN.algebra.CGroups