From 74aff044ef669bfa6d22ea27493edc03cf0e7c86 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sat, 21 Nov 2015 14:32:08 -0500
Subject: [PATCH] feat(group): port three more theorems from the standard
 library

---
 hott/algebra/group.hlean | 9 +++++++++
 hott/types/list.hlean    | 1 +
 2 files changed, 10 insertions(+)

diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index a438f845ca..852e7c4979 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -248,6 +248,15 @@ section group
   theorem mul_right_cancel {a b c : A} (H : a * b = c * b) : a = c :=
   by rewrite [-mul_inv_cancel_right a b, H, mul_inv_cancel_right]
 
+  theorem mul_eq_one_of_mul_eq_one {a b : A} (H : b * a = 1) : a * b = 1 :=
+  by rewrite [-inv_eq_of_mul_eq_one H, mul.left_inv]
+
+  theorem mul_eq_one_iff_mul_eq_one (a b : A) : a * b = 1 ↔ b * a = 1 :=
+  iff.intro !mul_eq_one_of_mul_eq_one !mul_eq_one_of_mul_eq_one
+
+  theorem eq_inv_of_mul_eq_one {a b : A} (H : a * b = 1) : a = b⁻¹ :=
+  (inv_eq_of_mul_eq_one (mul_eq_one_of_mul_eq_one H))⁻¹
+
   definition group.to_left_cancel_semigroup [instance] [reducible] : left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,
     mul_left_cancel := @mul_left_cancel A s ⦄
diff --git a/hott/types/list.hlean b/hott/types/list.hlean
index ab58630932..b1e9eb822c 100644
--- a/hott/types/list.hlean
+++ b/hott/types/list.hlean
@@ -869,6 +869,7 @@ theorem filter_append {p : A → Type} [h : decidable_pred p] : Π (l₁ l₂ :
   (suppose p a, by rewrite [append_cons, *filter_cons_of_pos _ this, filter_append])
   (suppose ¬ p a, by rewrite [append_cons, *filter_cons_of_neg _ this, filter_append])
 -/
+
 /- foldl & foldr -/
 definition foldl (f : A → B → A) : A → list B → A
 | a []       := a