Add In_elements_mem_iff

1 files changed, 15 insertions, 0 deletions

diff --git a/src/Util/MSetPositive/Facts.v b/src/Util/MSetPositive/Facts.v
index 26e2eadeb..3ccf5ad89 100644
--- a/src/Util/MSetPositive/Facts.v
+++ b/src/Util/MSetPositive/Facts.v
@@ -31,4 +31,19 @@ Module PositiveSetFacts.
     rewrite !elements_spec1.
     apply Hp.
   Qed.
+
+  Lemma In_elements_mem_iff {x p}
+    : List.In x (elements p) <-> PositiveSet.mem x p = true.
+  Proof using Type.
+    rewrite elements_b, existsb_exists; cbv [eqb].
+    repeat first [ apply conj
+                 | progress intros
+                 | progress destruct_head'_ex
+                 | progress destruct_head'_and
+                 | eexists
+                 | eassumption
+                 | break_innermost_match_step
+                 | break_innermost_match_hyps_step
+                 | congruence ].
+  Qed.
 End PositiveSetFacts.