proposition: Lemma ArcCos_Cos_inv : Feq (olor [0] Pi) (ArcCos[o]Cosine) FId.
proof: Proof. apply eq_imp_Feq. apply included_FComp. Included. intros. apply ArcCos_domain. apply less_wdr with (Cos x). 2: simpl in |- *; algebra. apply inv_cancel_less. astepr OneR. eapply leEq_less_trans. apply inv_leEq_AbsIR. inversion_clear X; apply Abs_Cos_less_One; auto. apply less_wdl with (Cos x). 2: simpl in |- *; algebra. eapply leEq_less_trans. apply leEq_AbsIR. inversion_clear X; apply Abs_Cos_less_One; auto. Included. intros. astepl (Part _ _ (ProjT2 Hx)); astepr x. cut (Dom ArcCos (Cos x)). intro H0. apply eq_transitive_unfolded with (ArcCos (Cos x) H0). apply pfwdef; simpl in |- *; algebra. inversion_clear X; apply ArcCos_Cos; auto. inversion_clear Hx. apply dom_wd with (Cosine x x0); auto. simpl in |- *; algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT