proposition: Lemma Cos_resp_less : forall x y, [0] [<=] x -> x [<] y -> y [<=] Pi -> Cos y [<] Cos x.
proof: Proof. intros x y H H0 H1. simpl in |- *. assert (Hab : [0] [<=] Pi [/]TwoNZ). apply less_leEq; apply pos_div_two; apply pos_Pi. assert (Hbc : Pi [/]TwoNZ [<=] Pi). apply less_leEq; apply pos_div_two'; apply pos_Pi. assert (Hac : [0] [<=] Pi). apply leEq_transitive with (Pi [/]TwoNZ); auto. apply strict_dec_glues with (Hab := Hab) (Hbc := Hbc) (Hac := Hac). Included. intros x0 y0 H2 H3 H4 Hx Hy. apply less_wdl with (Cos x0); [ apply less_wdr with (Cos y0) | idtac ]; [ idtac | simpl in |- *; algebra | simpl in |- *; algebra ]. inversion_clear H2; inversion_clear H3; apply Cos_resp_less_aux'; auto. intros x0 y0 H2 H3 H4 Hx Hy. apply less_wdl with (Cos x0); [ apply less_wdr with (Cos y0) | idtac ]; [ idtac | simpl in |- *; algebra | simpl in |- *; algebra ]. astepl (Cos [--]x0); astepl ( [--][--] (Cos [--]x0)); astepl ( [--] (Cos ( [--]x0[+]Pi))). apply less_wdl with ( [--] (Cos (Pi[-]x0))). 2: apply un_op_wd_unfolded; apply Cos_wd; rational. astepr (Cos [--]y0); astepr ( [--][--] (Cos [--]y0)); astepr ( [--] (Cos ( [--]y0[+]Pi))). apply less_wdr with ( [--] (Cos (Pi[-]y0))). 2: apply un_op_wd_unfolded; apply Cos_wd; rational. apply inv_resp_less. inversion_clear H2; inversion_clear H3; apply Cos_resp_less_aux'. apply shift_leEq_minus; astepl x0; auto. unfold cg_minus in |- *; apply plus_resp_leEq_less; [ apply leEq_reflexive | apply inv_resp_less; auto ]. apply shift_minus_leEq; apply shift_leEq_plus'; rstepl (Pi [/]TwoNZ); auto. split; auto; apply less_leEq; apply leEq_less_trans with x; auto. split; auto; apply less_leEq; apply less_leEq_trans with y; auto. auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac