proposition: Lemma cos1_gt0 : cos 1 > 0 :> R.
proof: Proof. have h := @cvg_cos_coeff' R 1; rewrite -(cvg_lim (@Rhausdorff R) h). apply: (@lt_trans _ _ (\sum_(0 <= i < 2) cos_coeff' 1 i)). rewrite big_nat_recr//= big_nat_recr//= big_nil add0r. rewrite /cos_coeff' expr0z expr1n fact0 !mul1r expr1n expr1z. by rewrite !mulNr subr_gt0 mul1r div1r ltf_pV2 ?posrE ?ltr0n// ltr_nat. apply: lt_sum_lim_series; [by move/cvgP in h|move=> d]. rewrite /cos_coeff' !(expr1n,mulr1). rewrite -muln2 -mulSn muln2 -exprnP -signr_odd odd_double expr0. rewrite -exprnP -signr_odd oddD/= muln2 odd_double/= expr1 add2n. rewrite mulNr subr_gt0 2!div1r ltf_pV2 ?posrE ?ltr0n ?fact_gt0//. by rewrite ltr_nat ltn_pfact//ltn_double doubleS. 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