proposition: Lemma Cos_resp_leEq : forall x y, [0] [<=] x -> y [<=] Pi -> x [<=] y -> Cos y [<=] Cos x.
proof: Proof. intros. astepl (Sin (Pi [/]TwoNZ[-]y)); astepr (Sin (Pi [/]TwoNZ[-]x)). apply Sin_resp_leEq. apply shift_leEq_minus; apply shift_plus_leEq'. unfold cg_minus in |- *; rstepr Pi; auto. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; auto. apply minus_resp_leEq_both. apply leEq_reflexive. auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac