proposition: Lemma cos_gt0_pihalf x : -(pi / 2) < x < pi / 2 -> 0 < cos x.
proof: Proof. wlog : x / 0 <= x => [Hw|x_ge0]. case: (leP 0 x) => [/Hw//| x_lt_0]. rewrite -{-1}[x]opprK ltrNl andbC [-- _ < _]ltrNl cosN. by apply: Hw => //; rewrite oppr_cp0 ltW. move=> /andP[x_gt0 xLpi2]; case: (ler0P (cos x)) => // cx_le0. have /IVT[]// : minr (cos 0) (cos x) <= 0 <= maxr (cos 0) (cos x). by rewrite cos0 /minr /maxr !ifN ?cx_le0 //= -leNgt (le_trans cx_le0). - by apply/continuous_subspaceT => ?; exact: continuous_cos. move=> x1 /itvP xx1 cx1_eq0. suff x1E : x1 = pi/2. have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite xx1. by rewrite x1E ltxx. apply: cos_02_uniq=> //; last by case pihalf_02_cos_pihalf => _ ->. by rewrite xx1 ltW // (lt_trans _ pihalf_lt2) // (le_lt_trans _ xLpi2) // xx1. by rewrite divr_ge0 ?(ltW pihalf_lt2)// pi_ge0. 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