diff options
| author | Kazuhiko Sakaguchi | 2020-05-16 09:02:13 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-05-16 09:30:39 +0900 |
| commit | 37a49513f22a3f792a1ac3241962a7d17455f7e5 (patch) | |
| tree | 3f3f5a094547ae1166a21cb7c5350c7e5a87404a /mathcomp/ssreflect/finset.v | |
| parent | 35bd8708dacfb508f896d957d7b1189ca7decb3e (diff) | |
A few more revisions
Diffstat (limited to 'mathcomp/ssreflect/finset.v')
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 9953c0d..e608d2b 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -900,7 +900,7 @@ Lemma subDset A B C : (A :\: B \subset C) = (A \subset B :|: C). Proof. apply/subsetP/subsetP=> sABC x; rewrite !inE. by case Bx: (x \in B) => // Ax; rewrite sABC ?inE ?Bx. -by case Bx: (x \in B) => //; move/sABC; rewrite inE Bx. +by case Bx: (x \in B) => // /sABC; rewrite inE Bx. Qed. Lemma subsetDP A B C : |