From fbb7b486e6dcd511142cbf173f01eccb4023e37c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 5 Feb 2018 11:03:17 +0100
Subject: tide up proof of card_inj_ffuns

---
 mathcomp/ssreflect/binomial.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

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 :
-- 
cgit v1.2.3