Add some lemmas about ex, and, eq

1 files changed, 26 insertions, 0 deletions

diff --git a/src/Util/Logic/ExistsEqAnd.v b/src/Util/Logic/ExistsEqAnd.v
new file mode 100644
index 000000000..27f08eb89
--- /dev/null
+++ b/src/Util/Logic/ExistsEqAnd.v
@@ -0,0 +1,26 @@
+Require Import Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Local Ltac t :=
+  repeat first [ progress destruct_head'_ex
+               | progress destruct_head'_and
+               | progress intros
+               | progress subst
+               | assumption
+               | progress repeat esplit ].
+
+Lemma ex_and_eq_l_iff {A P x}
+  : (exists y : A, y = x /\ P y) <-> P x.
+Proof. t. Qed.
+
+Lemma ex_and_eq_r_iff {A P x}
+  : (exists y : A, x = y /\ P y) <-> P x.
+Proof. t. Qed.
+
+Lemma ex_eq_and_l_iff {A P x}
+  : (exists y : A, P y /\ y = x) <-> P x.
+Proof. t. Qed.
+
+Lemma ex_eq_and_r_iff {A P x}
+  : (exists y : A, P y /\ x = y) <-> P x.
+Proof. t. Qed.