lemmas for proper and setC

1 files changed, 9 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index f4c1dd5..9bd8c1f 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -639,6 +639,9 @@ Proof. by apply/setP=> x; rewrite !inE. Qed.
 Lemma setCT : ~: [set: T] = set0.
 Proof. by rewrite -setC0 setCK. Qed.
 
+Lemma properC A B : (~: B \proper ~: A) = (A \proper B).
+Proof. by rewrite !properE !setCS. Qed.
+
 (* difference *)
 
 Lemma setDP A B x : reflect (x \in A /\ x \notin B) (x \in A :\: B).
@@ -982,6 +985,12 @@ Qed.
 Lemma properD A B C : (A \proper B :\: C) -> (A \proper B) && [disjoint A & C].
 Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed.
 
+Lemma properCr A B : (A \proper ~: B) = (B \proper ~: A).
+Proof. by rewrite -properC setCK. Qed.
+
+Lemma properCl A B : (~: A \proper B) = (~: B \proper A).
+Proof. by rewrite -properC setCK. Qed.
+
 End setOps.
 
 Arguments set1P {T x a}.