proposition: Lemma continuity_sin : continuity sin.
proof: Proof. unfold continuity; intro. assert (H0 := continuity_cos (PI / 2 - x)). unfold continuity_pt in H0; unfold continue_in in H0; unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; unfold Rdist in H0; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros. elim (H0 _ H); intros. exists x0; intros. elim H1; intros. split. - assumption. - intros; rewrite <- (cos_shift x); rewrite <- (cos_shift x1); apply H3. elim H4; intros. split. + unfold D_x, no_cond; split. * trivial. * red; intro; unfold D_x, no_cond in H5; elim H5; intros _ H8; elim H8; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive x1); apply Ropp_eq_compat; apply Rplus_eq_reg_l with (PI / 2); apply H7. + replace (PI / 2 - x1 - (PI / 2 - x)) with (x - x1); [ idtac | ring ]; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H6. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra