diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/ssreflect/finset.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/ssreflect/finset.v')
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index a9899b7..dc964b5 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -746,7 +746,7 @@ Lemma cardsU A B : #|A :|: B| = (#|A| + #|B| - #|A :&: B|)%N. Proof. by rewrite -cardsUI addnK. Qed. Lemma cardsI A B : #|A :&: B| = (#|A| + #|B| - #|A :|: B|)%N. -Proof. by rewrite -cardsUI addKn. Qed. +Proof. by rewrite -cardsUI addKn. Qed. Lemma cardsT : #|[set: T]| = #|T|. Proof. by rewrite cardsE. Qed. @@ -1969,7 +1969,7 @@ Qed. Lemma pblock_equivalence_partition : {in D &, forall x y, (y \in pblock P x) = R x y}. Proof. -have [_ tiP _] := and3P equivalence_partitionP. +have [_ tiP _] := and3P equivalence_partitionP. by move=> x y Dx Dy; rewrite /= (def_pblock tiP (PPx Dx) (Pxx Dx)) inE Dy. Qed. |