diff options
Diffstat (limited to 'mathcomp/algebra/ssrnum.v')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 0244891..a2a2395 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3462,7 +3462,7 @@ have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0. apply/leifP; case: ifPn => [/forall_inP-Econstant | Enonconstant]. have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0. have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const. - by rewrite exprMn_n prodrMn -(eq_bigr _ E_i) prodr_const. + by rewrite exprMn_n prodrMn_const -(eq_bigr _ E_i) prodr_const. set mu := \sum_(i in A) E i; pose En i := E i *+ n. pose cmp_mu s := [pred i | s * mu < s * En i]. have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}. @@ -3495,7 +3495,7 @@ have ->: \sum_(k in A') E' k = mu *+ n'. apply: (addrI mu); rewrite -mulrS -Dn -sumrMnl (bigD1 i Ai) big_andbC /=. rewrite !(bigD1 j A'j) /= addrCA eqxx !addrA subrK; congr (_ + _). by apply: eq_bigr => k /andP[_ /negPf->]. -rewrite prodrMn exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). +rewrite prodrMn_const exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). have ->: \prod_(k in A') E' k = E' j * pi. by rewrite (bigD1 j) //=; congr *%R; apply: eq_bigr => k /andP[_ /negPf->]. rewrite -(ler_pmul2l mu_gt0) -exprS -Dn mulrA; apply: lt_le_trans. |