proposition: Lemma Cos_nonneg : forall x, [--] (Pi [/]TwoNZ) [<=] x -> x [<=] Pi [/]TwoNZ -> [0] [<=] Cos x.
proof: Proof. simpl in |- *. intros; apply olor_pos_clcr_nonneg with ( [--] (Pi [/]TwoNZ)) (Pi [/]TwoNZ) I I. PiSolve. intros x0 H1 Hx; inversion_clear H1. apply less_wdr with (Cos x0); [ apply Cos_pos; auto | simpl in |- *; algebra ]. astepr (Cos [--] (Pi [/]TwoNZ)); apply eq_imp_leEq; Step_final (Cos (Pi [/]TwoNZ)). fold (Cos (Pi [/]TwoNZ)) in |- *; apply eq_imp_leEq; algebra. split; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac