proposition: Lemma cos_atan : forall x, cos (atan x) = 1/ (sqrt (1 + x ^ 2)).
proof: Proof. intro x ; destruct (exists_atan x) as [a [a_in Ha]] ; assert (cosa_pos : 0 < cos a) by (apply cos_pos ; assumption). rewrite <- Ha ; rewrite reciprocal_open_interval_atan_tan ; [| assumption]. unfold tan ; field_simplify (1 + (sin a / cos a) ^ 2). replace ((sin a) ^ 2 + (cos a) ^2) with (Rsqr (sin a) + Rsqr (cos a)) by (unfold Rsqr ; simpl ; ring). rewrite sin2_cos2. replace (1 / (cos a) ^ 2) with ((/cos a) * (/cos a)). rewrite sqrt_square. unfold Rdiv ; rewrite Rmult_1_l, Rinv_involutive. reflexivity. apply Rgt_not_eq ; assumption. left ; apply Rinv_0_lt_compat ; assumption. field. apply Rgt_not_eq ; assumption. apply Rgt_not_eq ; assumption. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5