From 4c7a2ecd1b35ce054d188c7fbf55e902a18fdde4 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 15 Dec 2017 13:41:41 +0100
Subject: [PATCH] Add the Pauli id law example

---
 FiniteSets/misc/dec_fset.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/FiniteSets/misc/dec_fset.v b/FiniteSets/misc/dec_fset.v
index bb0f4a3..2fea825 100644
--- a/FiniteSets/misc/dec_fset.v
+++ b/FiniteSets/misc/dec_fset.v
@@ -241,4 +241,13 @@ Section pauli.
     compute.
     apply tt.
   Defined.
+
+  Definition pauli_id x y : hProp := BuildhProp(Pauli_mult x y = y).
+
+  Theorem Pauli_mult_id : exist (fun x => all (fun y => pauli_id x y) Pauli_list) Pauli_list.
+  Proof.
+    refine (from_squash (exist _ _)).
+    compute.
+    apply tt.
+  Defined.
 End pauli.