proposition: Lemma Cos_ArcCos_inv : Feq (olor [--][1] [1]) (Cosine[o]ArcCos) FId.
proof: Proof. apply eq_imp_Feq. apply included_FComp. unfold ArcCos in |- *; Included. intros; apply cos_domain. Included. intros. inversion_clear Hx. astepr x; astepl (Part _ _ (ProjT2 Hx)); astepl (Part _ _ X0). apply eq_transitive_unfolded with (Cos (ArcCos x x0)). simpl in |- *; algebra. apply eq_symmetric_unfolded; apply Cos_ArcCos. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT