From f3640db250f55bdb8d9d379d078586349b03e856 Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Sun, 30 Oct 2016 21:42:07 -0400
Subject: Added new algebra lemma

---
 src/Algebra.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Algebra.v b/src/Algebra.v
index c017a7456..de6b6f51a 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -378,6 +378,13 @@ Module Group.
       apply inv_id.
     Qed.
 
+    Lemma inv_zero_zero : forall x, inv x = id -> x = id.
+    Proof.
+      intros.
+      rewrite <-inv_id, <-H0.
+      symmetry; apply inv_inv.
+    Qed.
+
     Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c.
     Proof.
       split; intro Hx; rewrite Hx || rewrite <-Hx;
-- 
cgit v1.2.3