proposition: Lemma Sin_ArcSin_inv : Feq (olor [--][1] [1]) (Sine[o]ArcSin) FId.
proof: Proof. apply eq_imp_Feq. apply included_FComp. Included. intros; apply sin_domain. Included. intros x H Hx Hx'. elim Hx; intros x0 H0. astepr x; astepl (Part _ _ (ProjT2 Hx)); astepl (Part _ _ H0). apply eq_transitive_unfolded with (Sin (ArcSin x x0)). simpl in |- *; algebra. apply eq_symmetric_unfolded; apply Sin_ArcSin. algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT