proposition: Lemma R_tan_as_IR : forall x dom, RasIR (tan x) [=] Tan (RasIR x) dom.
proof: Proof. intros x dom. unfold tan. cut (Dom (f_rcpcl' IR) (RasIR (cos x))). intro Hdiv. rewrite -> (R_div_as_IR (sin x) (cos x) Hdiv). cut (Dom (f_rcpcl' IR) (Cos (RasIR x))). intro ndom. stepl (Sin(RasIR x) [/] Cos(RasIR x) [//] ndom). unfold Tan. unfold Tang. apply: div_wd. apply: pfwdef. reflexivity. apply: pfwdef. reflexivity. apply div_wd. symmetry; apply R_sin_as_IR. symmetry; apply R_cos_as_IR. unfold pfdom,f_rcpcl' in *. stepl (RasIR (cos x)); [| now apply R_cos_as_IR]. assumption. unfold pfdom,f_rcpcl', Tang,Fdiv in *. destruct dom. destruct e. stepl (Cos (RasIR x)); [| now symmetry; apply R_cos_as_IR]. apply: c. Qed.
imports: Coq.QArith.QArith Coq.QArith.Qreals Coq.QArith.QArith_base CoRN.tactics.CornTac Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun CoRN.coq_reals.Rreals CoRN.reals.iso_CReals CoRN.reals.CauchySeq Coq.Reals.Rtrigo_def CoRN.transc.PowerSeries Coq.Logic.ConstructiveEpsilon Coq.Reals.Rlogic Coq.Reals.Reals CoRN.transc.Pi CoRN.transc.MoreArcTan CoRN.logic.PropDecid CoRN.transc.Exponential Coq(Lia Lra)