proposition: Lemma cosK : {in `[0, pi], cancel cos acos}.
proof: Proof. move=> x xB; apply: cos_inj => //; rewrite ?acosK//; last first. by move: xB; rewrite !in_itv/= => /andP[? ?];rewrite cos_geN1 cos_le1. move: xB; rewrite !in_itv/= => /andP[? ?]. by rewrite acos_ge0 ?acos_lepi ?cos_geN1 ?cos_le1. 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