proposition: Lemma tan_inj : {in `](- (pi/2)), (pi/2)[ &, injective tan}.
proof: Proof. move=> x y xB yB tanE. by case: (ltrgtP x y); rewrite // -ltr_tan ?tanE ?ltxx. 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