proposition: Lemma ArcCos_Cos : forall x, [0] [<] x -> x [<] Pi -> forall H, ArcCos (Cos x) H [=] x.
proof: Proof. intros x H H0 H1. assert (H2 : Dom ArcCos (Sin (Pi [/]TwoNZ[-]x))). apply dom_wd with (Cos x); algebra. astepl (Part _ _ H2). unfold ArcCos in |- *. astepl (Pi [/]TwoNZ[-]Part _ _ (ProjIR2 H2)). rstepr (Pi [/]TwoNZ[-] (Pi [/]TwoNZ[-]x)). apply cg_minus_wd. algebra. apply ArcSin_Sin. apply shift_less_minus; apply shift_plus_less'. rstepr Pi; auto. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; auto. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT