proposition: Lemma ltr_sin : {in `[ (- (pi/2)), pi/2] &, {mono sin : x y / x < y}}.
proof: Proof. move=> x y /itvP xpi /itvP ypi; rewrite -[sin x]opprK ltrNl. rewrite -!cosDpihalf -[x < y](ltrD2r (pi /2)) ltr_cos// !in_itv/=. - by rewrite -lerBlDr sub0r xpi/= [leRHS]splitr lerD2r xpi. - by rewrite -lerBlDr sub0r ypi/= [leRHS]splitr lerD2r ypi. 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