proposition: Lemma Cos_ArcCos : forall (x : IR) Hx, x [=] Cos (ArcCos x Hx).
proof: Proof. intros. unfold ArcCos in |- *. astepr (Cos (Pi [/]TwoNZ[-]ArcSin x (ProjIR2 Hx))). astepr (Sin (ArcSin x (ProjIR2 Hx))). apply Sin_ArcSin. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT