proposition: Lemma ltr_tan : {in `](- (pi/2)), (pi/2)[ &, {mono tan : x y / x < y}}.
proof: Proof. move=> x y; wlog xLy : x y / x <= y => [H xB yB|/itvP xB /itvP yB]. 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 -subr_gt0 xLLs; rewrite -subr_gt0 in xLLs; apply/idP. have [x1 /itvP x1I|z |] := @MVT_segment _ tan (fun x => (cos x) ^-2) _ _ xLy. - apply: is_derive_tan. rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _ _ x) ?x1I ?xB//=. by rewrite (@le_lt_trans _ _ y) ?x1I ?yB. - apply/continuous_in_subspaceT => ? -/[!(@mem_setE R)] /itvP inI. apply: continuous_tan; rewrite gt_eqF// cos_gt0_pihalf//. by rewrite (@lt_le_trans _ _ x) ?xB ?inI// (@le_lt_trans _ _ y) ?yB ?inI. - move=> x1 /itvP x1I ->. rewrite mulr_gt0 // invr_gt0 // exprn_gte0 // cos_gt0_pihalf //. by rewrite (@lt_le_trans _ _ x) ?x1I ?xB//= (@le_lt_trans _ _ y) ?x1I ?yB. 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