diff options
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 1f0ae16..c99e296 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -365,10 +365,10 @@ Lemma card_inj_ffuns_on D T (R : pred T) : Proof. rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. - by exists val => // x _; apply: val_inj. -rewrite -(on_card_preimset (bijFF _)); apply: eq_card => t. -rewrite !inE -(codom_ffun (Finfun t)); congr (_ && _); apply: negb_inj. -by rewrite -has_predC has_map enumT has_filter -size_eq0 -cardE. + by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. +rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. +rewrite !inE -(big_andE predT) -big_filter big_all -all_map. +by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK. Qed. Lemma card_inj_ffuns D T : |