diff options
| author | Enrico Tassi | 2018-02-05 11:03:17 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-02-05 11:04:41 +0100 |
| commit | fbb7b486e6dcd511142cbf173f01eccb4023e37c (patch) | |
| tree | d0148d635af78b8fb6d1058d490af1bae6714e0c /mathcomp | |
| parent | 64c6b07ff318b9eee032e929f0cd25b2e2ddaeda (diff) | |
tide up proof of card_inj_ffuns
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index d683768..e42b1fd 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -375,7 +375,7 @@ Lemma card_inj_ffuns D T : #|[set f : {ffun D -> T} | injectiveb f]| = #|T| ^_ #|D|. Proof. rewrite -card_inj_ffuns_on; apply: eq_card => f. -by rewrite 2!inE; case: ffun_onP => // []. +by rewrite 2!inE; case: ffun_onP. Qed. Lemma cards_draws T (B : {set T}) k : |