proposition: Lemma Cos_resp_less_aux : forall x y : IR, [0] [<] x -> x [<] y -> y [<=] Pi [/]TwoNZ -> Cos y [<] Cos x.
proof: Proof. intros x y H H0 H1. astepl (Cos y[+][0]). apply shift_plus_less'. assert (H2 : Continuous_I (less_leEq _ _ _ H0) Sine). apply included_imp_Continuous with realline; Contin. assert (H3 : Continuous_I (Min_leEq_Max x y) Sine). apply included_imp_Continuous with realline; Contin. assert (H4 : Continuous_I (Min_leEq_Max y x) Sine). apply included_imp_Continuous with realline; Contin. assert (H5 : Continuous_I (Min_leEq_Max y x) {--}Sine). apply included_imp_Continuous with realline; Contin. apply less_leEq_trans with (Sin x[*] (y[-]x)). apply mult_resp_pos. apply Sin_pos; auto. apply less_transitive_unfolded with (Pi [/]TwoNZ). apply less_leEq_trans with y; auto. PiSolve. apply shift_less_minus; astepl x; auto. apply leEq_wdr with (Integral H3). eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply (Integral_integral _ _ _ _ H3 _ H2). apply lb_integral. intros z H6 Hx. apply leEq_wdr with (Sin z). 2: simpl in |- *; algebra. cut ( [--] (Pi [/]TwoNZ) [<=] x); intros. inversion_clear H6; apply Sin_resp_leEq; auto. apply leEq_transitive with y; auto. apply leEq_transitive with ZeroR; PiSolve. astepl ( [--][--] (Integral H3)). apply eq_transitive_unfolded with ( [--] (Integral H4)). apply un_op_wd_unfolded; apply eq_symmetric_unfolded; apply Integral_op. apply eq_transitive_unfolded with (Integral H5). apply eq_symmetric_unfolded; apply Integral_inv. assert (H6 : Derivative realline I Cosine {--}Sine). Deriv. eapply eq_transitive_unfolded. apply Barrow with (derG0 := H6) (Ha := I) (Hb := I) (pJ := I); Contin; split. simpl in |- *; algebra. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac