diff options
| author | Cyril Cohen | 2019-03-20 18:31:45 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-03-24 00:04:29 +0100 |
| commit | 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 (patch) | |
| tree | fc3fdae51954678506ab64575e1ef33eb8485525 /mathcomp/ssreflect/binomial.v | |
| parent | 794cfe568c2b2e1eb138a8f881c330838d8a3c2d (diff) | |
Compat of sumn with bigop and renaming dep to cond when appropriate
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -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 98ee64e..1f0ae16 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -387,7 +387,7 @@ have [ltTk | lekT] := ltnP #|B| k. have [AsubB /=|//] := boolP (A \subset B). by rewrite (leq_ltn_trans (subset_leq_card AsubB)) ?andbF. apply/eqP; rewrite -(eqn_pmul2r (fact_gt0 k)) bin_ffact // eq_sym. -rewrite -sum_nat_dep_const -{1 3}(card_ord k). +rewrite -sum_nat_cond_const -{1 3}(card_ord k). rewrite -card_inj_ffuns_on -sum1dep_card. pose imIk (f : {ffun 'I_k -> T}) := f @: 'I_k. rewrite (partition_big imIk (fun A => (A \subset B) && (#|A| == k))) /= |