proposition: Lemma cosatanspos : forall x:R, cos(atan x)>0.
proof: Proof. intro. apply cos_gt_0. rewrite<-Ropp_div. apply (proj1 (atan_bound _)). apply (proj2 (atan_bound _)). Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra