proposition: Lemma ltr_cos : {in `[0, pi] &, {mono cos : x y /~ y < x}}.
proof: Proof. move=> x y; rewrite !in_itv/= le_eqVlt; case: eqP => [<- _|_] /=. rewrite cos0 le_eqVlt; case: eqP => /= [<- _|_ /andP[y_gt0 gLpi]]. by rewrite cos0 !ltxx. rewrite y_gt0; apply/idP. suff : cos y != 1 by case: ltrgtP (cos_le1 y). rewrite -cos0 eq_sym; apply/eqP => /Rolle [||x1|x1 /itvP x1I [_ x1D]] //. by apply/continuous_subspaceT => ?; exact: continuous_cos. case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0. suff : 0 < sin x1 by rewrite s_eq0 ltxx. by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < y)) ?x1I // yI. rewrite le_eqVlt; case: eqP => [-> _ /andP[y_ge0]|/= _ /andP[x_gt0 x_ltpi]] /=. rewrite cospi le_eqVlt; case: eqP => /= [-> _|/eqP yDpi y_ltpi]. by rewrite cospi ltxx. by rewrite ltNge cos_geN1 ltNge ltW. rewrite le_eqVlt; case: eqP => [<- _|_] /=. rewrite cos0 [_ < 0]ltNge ltW //=. by apply/idP/negP; rewrite -leNgt cos_le1. rewrite le_eqVlt; case: eqP => /= [-> _ | _ /andP[y_gt0 y_ltpi]]. rewrite cospi x_ltpi; apply/idP. suff : cos x != -1 by case: ltrgtP (cos_geN1 x). rewrite -cospi; apply/eqP => /Rolle [||x1|x1 /itvP x1I [_ x1D]] //. by apply/continuous_subspaceT => ?; exact: continuous_cos. case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0. suff : 0 < sin x1 by rewrite s_eq0 ltxx. by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < x)) ?x1I. wlog xLy : x y x_gt0 x_ltpi y_gt0 y_ltpi / x <= y => [H | ]. case: (lerP x y) => [/H //->//|yLx]. by rewrite !ltNge ltW ?(ltW yLx) // H // ltW. case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx. have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. rewrite xLLs -subr_gt0 -opprB; rewrite -subr_gt0 in xLLs; apply/idP. have [x1|z /itvP zI ->] := @MVT_segment _ cos (- sin) _ _ xLy. by apply/continuous_subspaceT => ?; exact: continuous_cos. rewrite -mulNr opprK mulr_gt0 //; apply: sin_gt0_pi. by rewrite (lt_le_trans x_gt0) ?zI //= (le_lt_trans _ y_ltpi) ?zI. 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