proposition: Lemma ArcSin_resp_leEq : forall x y, [--][1] [<] x -> x [<=] y -> y [<] [1] -> forall Hx Hy, ArcSin x Hx [<=] ArcSin y Hy.
proof: Proof. intros x y H H0 H1 Hx Hy. assert (H2 : [--][1] [<] OneR). apply less_transitive_unfolded with ZeroR; [ astepr ( [--]ZeroR); apply inv_resp_less | idtac ]; apply pos_one. apply Derivative_imp_resp_leEq with (olor [--][1] [1]) H2 (( [-C-][1]{-}FId{^}2) {!} [-C-] [--] ([1] [/]TwoNZ)); Deriv. intros; apply leEq_glb; intro z; intros. elim Hy0; intros. apply leEq_wdr with (Exp (( [-C-] [--] ([1] [/]TwoNZ) {*} (Logarithm[o] [-C-][1]{-}FId{^}2)) z x0)). apply less_leEq; apply Exp_pos. simpl in |- *; algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT