predeqP missing, as mentioned on Zulip, statement found in PR#282

math-comp · Dec 17, 2020 · 90154a3 · 90154a3
1 parent 4f920ad
commit 90154a3
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `classical_sets.v`:
+  + lemma `predeqP`
+
 ### Changed
 
 ### Renamed

diff --git a/theories/classical_sets.v b/theories/classical_sets.v
@@ -265,6 +265,9 @@ rewrite propeqE; split => [->|[FG GF]]; [by split|].
 by rewrite predeqE => t; split=> [/FG|/GF].
 Qed.
 
+Lemma predeqP T (A B : set T) : (A = B) <-> (A `<=>` B).
+Proof. by rewrite eqEsubset. Qed.
+
 Lemma eq_set T (P Q : T -> Prop): (forall x : T, P x = Q x) ->
   [set x | P x] = [set x | Q x].
 Proof. by move=> /funext->. Qed.