proposition: Lemma atan1 : atan 1 = pi / 4%:R :> R.
proof: Proof. apply: tan_inj; first 2 last. by rewrite atanK tan_piquarter. by rewrite in_itv/= atan_gtNpi2 atan_ltpi2. rewrite in_itv/= -mulNr (lt_trans _ (_ : 0 < _ )) /=; last 2 first. by rewrite mulNr oppr_cp0 divr_gt0 // pi_gt0. by rewrite divr_gt0 ?pi_gt0 // ltr0n. rewrite ltr_pdivrMr// -mulrA ltr_pMr// ?pi_gt0//. by rewrite (natrM _ 2 2) mulrA mulVf// mul1r ltr1n. 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