proposition: Lemma cos2_lt0 : cos 2 < 0 :> R.
proof: Proof. rewrite -(opprK (cos _)) oppr_lt0; have /cvgN h := @cvg_cos_coeff' R 2. rewrite -(cvg_lim (@Rhausdorff R) h). apply: (@lt_trans _ _ (\sum_(0 <= i < 3) - cos_coeff' 2 i)). do 3 rewrite big_nat_recl//; rewrite big_nil addr0 3!cos_coeff'E double0. rewrite cos_coeff_2_0 cos_coeff_2_2 -muln2 cos_coeff_2_4 addrA -(opprD 1). rewrite opprB -(@natrB _ 2 1)// subn1/= -[in X in X - _](@divff _ 3%:R)//. by rewrite -mulrBl divr_gt0// -natrB// -[(_ - _)%N]/_.+1. rewrite -seriesN lt_sum_lim_series //. by move/cvgP in h; by rewrite seriesN. move=> d. rewrite /cos_coeff' 2!exprzD_nat (exprSz _ d.*2) -[in (-1) ^ d.*2](muln2 d). rewrite -(exprnP _ (d * 2)) (exprM (-1)) sqrr_sign 2!mulr1 -exprSzr. rewrite (_ : 4 = 2 * 2)%N // -(exprnP _ (2 * 2)) (exprM (-1)) sqrr_sign. rewrite mul1r [(-1) ^ 3](_ : _ = -1) ?mulN1r ?mulNr ?opprK; last first. by rewrite -exprnP 2!exprS expr1 mulrN1 opprK mulr1. rewrite subr_gt0. rewrite addnS doubleS -[X in 2 ^+ X]addn2 exprD -mulrA ltr_pM2l//. rewrite factS factS 2!natrM mulrA invfM !mulrA. rewrite ltr_pdivrMr ?ltr0n ?fact_gt0// mulVf ?pnatr_eq0 ?gtn_eqF ?fact_gt0//. rewrite ltr_pdivrMr ?mul1r //. by rewrite expr2 -!natrM ltr_nat !mulSn !add2n mul0n !addnS. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp