proposition: Lemma Cos_resp_less_aux' : forall x y : IR, [0] [<=] x -> x [<] y -> y [<=] Pi [/]TwoNZ -> Cos y [<] Cos x.
proof: Proof. intros. apply less_leEq_trans with (Cos ((x[+]y) [/]TwoNZ)). apply Cos_resp_less_aux; auto. apply pos_div_two; astepl (ZeroR[+][0]); apply plus_resp_leEq_less; try apply leEq_less_trans with x; auto. apply shift_div_less; [ apply pos_two | apply shift_plus_less ]. rstepr y; auto. apply Cos_resp_leEq; auto. apply shift_div_leEq. apply pos_two. rstepr (Pi [/]TwoNZ[+]Pi [/]TwoNZ[+]Pi). astepl (x[+]y[+][0]). repeat apply plus_resp_leEq_both; auto. apply less_leEq; apply less_leEq_trans with y; auto. PiSolve. apply shift_leEq_div; [ apply pos_two | apply shift_leEq_plus' ]. rstepl x; apply less_leEq; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac