proposition: Lemma sin_inj : {in `[(- (pi/2)), (pi/2)] &, injective sin}.
proof: Proof. move=> x y /itvP xpi /itvP ypi sinE; have : - sin x = - sin y by rewrite sinE. rewrite -!cosDpihalf => /cos_inj h; apply/(addIr (pi/2))/h; rewrite !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