Merge pull request #2189 from Alizter/ps/rr/group_unit_lemmas

group unit lemmas

theories/Algebra/AbGroups/Centralizer.v

@@ -11,10 +11,8 @@ Local Open Scope mc_mult_scope.
 Definition centralizer {G : Group} (g : G)
   := fun h => g * h = h * g.
 
-Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit.
-Proof.
-  exact (grp_unit_r _ @ (grp_unit_l _)^).
-Defined.
+Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit
+  := grp_g1_1g _ _ idpath.
 
 Definition centralizer_sgop {G : Group} (g h k : G)
            (p : centralizer g h) (q : centralizer g k)
@@ -33,7 +31,7 @@ Definition centralizer_inverse {G : Group} (g h : G)
 Proof.
   unfold centralizer in *.
   symmetry.
-  refine ((grp_unit_r _)^ @ _ @ grp_unit_l _).
+  apply grp_g1_1g.
   refine (ap ((_ * g) *.) (grp_inv_r h)^ @ _ @ ap (.* (g * _)) (grp_inv_l h)).
   refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^).
   refine (ap (.* h^) _).

theories/Algebra/Groups/Group.v

@@ -465,6 +465,12 @@ Section GroupEquations.
   Definition grp_inv_gV_g : (x * y^) * y = x
     := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_l y) @ grp_unit_r x.
 
+  Definition grp_1g_g1 : x = y <~> 1 * x = y * 1
+    := equiv_concat_r (grp_unit_r _)^ _ oE equiv_concat_l (grp_unit_l _) _.
+
+  Definition grp_g1_1g : x = y <~> x * 1 = 1 * y
+    := equiv_concat_r (grp_unit_l _)^ _ oE equiv_concat_l (grp_unit_r _) _.
+
 End GroupEquations.
 
 (** ** Cancelation lemmas *)
@@ -678,7 +684,7 @@ Definition grp_pow_commutes {G : Group} (n : Int) (g h : G)
   : h * (grp_pow g n) = (grp_pow g n) * h.
 Proof.
   induction n.
-  - exact (grp_unit_r _ @ (grp_unit_l _)^).
+  - by apply grp_g1_1g.
   - rewrite grp_pow_succ.
     nrapply grp_commutes_op; assumption.
   - rewrite grp_pow_pred.
@@ -1168,8 +1174,7 @@ Definition grp_conj_unit {G : Group} : grp_conj (G:=G) 1 $== Id _.
 Proof.
   intros x.
   apply grp_moveR_gV.
-  rhs nrapply grp_unit_r.
-  nrapply grp_unit_l.
+  by nrapply grp_1g_g1.
 Defined.
 
 (** Conjugation commutes with group homomorphisms. *)