diff options
| author | Assia Mahboubi | 2018-02-05 11:54:56 +0100 |
|---|---|---|
| committer | GitHub | 2018-02-05 11:54:56 +0100 |
| commit | 835467324db450c8fb8971e477cc4d82fa3e861b (patch) | |
| tree | d0148d635af78b8fb6d1058d490af1bae6714e0c | |
| parent | 64c6b07ff318b9eee032e929f0cd25b2e2ddaeda (diff) | |
| parent | fbb7b486e6dcd511142cbf173f01eccb4023e37c (diff) | |
Merge pull request #176 from gares/fix/card_inj_ffuns
tide up proof of card_inj_ffuns
| -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 : |