proposition: Lemma tan_piquarter : tan (pi / 4%:R) = 1.
proof: Proof. rewrite /tan -cosBpihalf (splitr (pi / 2)) opprD addrA -mulrA -invfM -natrM. rewrite subrr sub0r cosN divff// gt_eqF// cos_gt0_pihalf//. rewrite ltr_pM2l ?pi_gt0// ltf_pV2 ?qualifE//= ltr_nat andbT. by rewrite (@lt_trans _ _ 0)// ?oppr_lt0 ?divr_gt0 ?pi_gt0. 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