From 88b1305ed18f783c7ec8e16ae8da1f932303742c Mon Sep 17 00:00:00 2001
From: thery
Date: Thu, 15 Sep 2016 17:39:55 +0200
Subject: 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
---
 mathcomp/odd_order/PFsection9.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/odd_order')

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