proposition: Lemma ArcSin_Sin : forall x, [--] (Pi [/]TwoNZ) [<] x -> x [<] Pi [/]TwoNZ -> forall H, ArcSin (Sin x) H [=] x.
proof: Proof. intros. unfold Sin in |- *. astepr (FId x I). cut (Dom (ArcSin[o]Sine) x). intro H2. apply eq_transitive_unfolded with ((ArcSin[o]Sine) x H2). simpl in |- *; algebra. apply Feq_imp_eq with (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)). apply ArcSin_Sin_inv. split; auto. exists I; auto. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT