proposition: Lemma cos_exists : exists2 pih : R, 1 <= pih <= 2 & cos pih = 0.
proof: Proof. have /IVT[] : minr (cos 1) (cos 2) <= (0 : R) <= maxr (cos 1) (cos 2). - by rewrite le_maxr (ltW cos1_gt0) le_minl (ltW cos2_lt0) orbC. - by rewrite ler1n. - by apply/continuous_subspaceT => ?; exact: continuous_cos. by move=> pih /itvP pihI chpi_eq0; exists pih; rewrite ?pihI. 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