diff options
| author | thery | 2016-09-15 17:39:55 +0200 |
|---|---|---|
| committer | thery | 2016-09-16 13:14:28 +0200 |
| commit | 88b1305ed18f783c7ec8e16ae8da1f932303742c (patch) | |
| tree | 615f06ea5cd108606427121f8b760ceda152eaf1 /mathcomp/odd_order/PFsection9.v | |
| parent | 9c4f68936e33c93cf179eec6e996062bec918915 (diff) | |
Refactoring of binonial
Variable renaming from 'C(m,n) to 'C(n,m)
Renaming theorem mul_Sm_binn to mul_bin_diag
Adding theorems mul_bin_left mul_bin_right
Diffstat (limited to 'mathcomp/odd_order/PFsection9.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection9.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index 63e10bb..e7f82bc 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.v @@ -1953,7 +1953,7 @@ have [gtS4alpha s4gt0]: (size S4)%:R > '[alpha] /\ (size S4 > 0)%N. rewrite ltn_pmul2r ?expn_gt0 ?a_gt0 // -doubleS. by rewrite -(prednK q_gt0) expnS mul2n leq_double ltn_expl. rewrite mulnA leq_pmul2r ?expn_gt0 ?a_gt0 // -(subnKC q_gt2). - rewrite mulnCA mulnA addSn -mul_Sm_binm bin1 -mulnA leq_pmul2l //. + rewrite mulnCA mulnA addSn -mul_bin_diag bin1 -mulnA leq_pmul2l //. by rewrite mulnS -addSnnS leq_addr. rewrite Dp -Da_p mul2n (addnC a.*2) expnDn -(subnKC q_gt2) !addSn add0n. rewrite 3!big_ord_recl big_ord_recr /= !exp1n /= bin1 binn !mul1n /bump /=. |