proposition: Lemma cos_atan x : cos (atan x) = (Num.sqrt (1 + x ^+ 2)) ^-1.
proof: Proof. have cos_gt0 : 0 < cos (atan x). by apply: cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2. have cosD0 : cos (atan x) != 0 by apply: lt0r_neq0. have /eqP : cos (atan x) ^+2 = (Num.sqrt (1 + x ^+ 2))^-2. by rewrite -[LHS]invrK cos2_tan2 // atanK sqr_sqrtr // addr_ge0 // sqr_ge0. rewrite -exprVn eqf_sqr => /orP[] /eqP // cosE. move: cos_gt0; rewrite cosE ltNge; case/negP. by rewrite oppr_le0 invr_ge0 sqrtr_ge0. 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