proposition: Lemma cos_ge0_pihalf x : -(pi / 2) <= x <= pi / 2 -> 0 <= cos x.
proof: Proof. rewrite le_eqVlt; case: (_ =P x) => /= [<-|_]. by rewrite cosN cos_pihalf. rewrite le_eqVlt; case: (x =P _) => /= [->|_ H]; first by rewrite cos_pihalf. by rewrite ltW //; apply: cos_gt0_pihalf. 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