proposition: Lemma ArcCos_resp_leEq : forall x y, [--][1] [<] x -> x [<=] y -> y [<] [1] -> forall Hx Hy, ArcCos y Hy [<=] ArcCos x Hx.
proof: Proof. intros. Opaque ArcSin. simpl in |- *; unfold cg_minus in |- *; apply plus_resp_leEq_lft. apply inv_resp_leEq; apply ArcSin_resp_leEq; auto. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT