proposition: Lemma atan_sub_correct : forall u v, 1 + u * v <> 0 -> -PI/2 < atan u - atan v < PI/2 -> -PI/2 < atan (atan_sub u v) < PI/2 -> atan u = atan v + atan (atan_sub u v).
proof: Proof. intros u v pn0 uvint aint. assert (cos (atan u) <> 0). { destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto. rewrite <- Rdiv_opp_l; assumption. } assert (cos (atan v) <> 0). { destruct (atan_bound v); apply Rgt_not_eq, cos_gt_0; auto. rewrite <- Rdiv_opp_l; assumption. } assert (t : forall a b c, a - b = c -> a = b + c) by (intros; subst; field). apply t, tan_inj; clear t; try assumption. rewrite tan_minus; auto. - rewrite !tan_atan; reflexivity. - apply Rgt_not_eq, cos_gt_0; rewrite <- ?Rdiv_opp_l; tauto. - rewrite !tan_atan; assumption. Qed.
imports: Lia Lra Rbase Rtrigo1 Ranalysis_reg Rfunctions AltSeries Rseries SeqProp PartSum Ratan