proposition: Lemma sin2_gt0 x : 0 < x < 2 -> 0 < sin x.
proof: Proof. move=> /andP[x_gt0 x_lt2]. have sinx := @cvg_sin_coeff' _ x. rewrite -(cvg_lim (@Rhausdorff R) sinx). rewrite [ltLHS](_ : 0 = \sum_(0 <= i < 0) sin_coeff' x i :> R); last first. by rewrite big_nil. apply: lt_sum_lim_series; first by move/cvgP in sinx. move=> d. rewrite /sin_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 !add0n!mul1r mulN1r -[d.*2.+1]addn1 doubleD -addSn exprD. rewrite -(ffact_fact (leq_addl _ _)) addnK. rewrite mulNr -!mulrA -mulrBr mulr_gt0 ?exprn_gt0 //. set u := _.+1. rewrite natrM invfM. rewrite -[X in _ < X - _]mul1r !mulrA -mulrBl divr_gt0 //; last first. by rewrite (ltr_nat _ 0) fact_gt0. rewrite subr_gt0. set v := _ ^_ _; rewrite -[ltRHS](divff (_ : v%:R != 0)); last first. by rewrite lt0r_neq0 // (ltr_nat _ 0) ffact_gt0 leq_addl. rewrite ltr_pM2r; last by rewrite invr_gt0 (ltr_nat _ 0) ffact_gt0 leq_addl. rewrite {}/v !addnS addn0 !ffactnS ffactn0 muln1 /= natrM. by rewrite (ltr_pM (ltW _ ) (ltW _)) // (lt_le_trans x_lt2) // ler_nat. 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