diff options
| author | Cyril Cohen | 2019-03-26 13:48:38 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-26 13:48:38 +0100 |
| commit | 5c5455be722fe60634f511c876e05e3201091e25 (patch) | |
| tree | f9cbe81a565d7d9634bcb4a84ffcb572986cd6d9 /mathcomp/ssreflect/binomial.v | |
| parent | 07f9f2b983f4e61d4dc930146d3823b485f35b91 (diff) | |
| parent | 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 (diff) | |
Merge pull request #305 from CohenCyril/sumn
compat sumn with bigop
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))) /= |