proposition: Lemma cos_inj : {in `[0,pi] &, injective (@cos R)}.
proof: Proof. move=> x y x0pi y0pi xy; apply/eqP; rewrite eq_le; apply/andP; split. - by have := ltr_cos y0pi x0pi; rewrite xy ltxx => /esym/negbT; rewrite -leNgt. - by have := ltr_cos x0pi y0pi; rewrite xy ltxx => /esym/negbT; rewrite -leNgt. 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