proposition: Lemma cosatan : forall x:R, Rsqr (cos(atan x))=(/(1+Rsqr x))%R.
proof: Proof. intro. rewrite<-(atan_right_inv x) at 2. unfold tan. rewrite Rsqr_div. rewrite sin2. unfold Rsqr. field. split. apply (Rlt_neq _ _ (cosatanspos _)). unfold Rminus. rewrite Rplus_comm. rewrite Rplus_assoc. Rsimpl. apply R1_neq_R0. apply (Rlt_neq _ _ (cosatanspos _)). Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra