proposition: Lemma bnd_Cos : bnd_away_zero_in_P Cosine (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)).
proof: Proof. intros a b Hab H. split. Included. set (pos2 := less_leEq _ _ _ (pos_two IR)) in *. assert (H0 : [0] [<] sqrt Two pos2). apply power_cancel_less with 2. apply sqrt_nonneg. astepl ZeroR; astepr (Two:IR); apply pos_two. set (Hsqrt := pos_ap_zero _ _ H0) in *. exists (Min (Min (Cos a) (Cos b)) ([1][/] _[//]Hsqrt)). elim (H _ (compact_inc_lft _ _ Hab)); intros. elim (H _ (compact_inc_rht _ _ Hab)); intros. repeat apply less_Min; try apply Cos_pos; auto. apply recip_resp_pos. apply power_cancel_less with 2. apply sqrt_nonneg. astepl ZeroR; astepr (Two:IR); apply pos_two. intros y Hy X. apply leEq_wdr with (Cos y). 2: apply eq_transitive_unfolded with (AbsIR (Cos y)). 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply less_leEq; elim (H y X); intros; apply Cos_pos; auto. 2: apply AbsIR_wd; simpl in |- *; algebra. elim (less_cotransitive_unfolded _ _ _ pos_QuarterPi y); intros. eapply leEq_transitive. apply Min_leEq_lft. apply leEq_transitive with (Cos b). apply Min_leEq_rht. elim (H _ (compact_inc_rht _ _ Hab)); elim (H y X); intros. inversion_clear X. apply Cos_resp_leEq; auto; apply less_leEq; auto. apply less_transitive_unfolded with (Pi [/]TwoNZ); PiSolve. elim (less_cotransitive_unfolded _ _ _ neg_invQuarterPi y); intros. 2: eapply leEq_transitive. 2: apply Min_leEq_lft. 2: apply leEq_transitive with (Cos a). 2: apply Min_leEq_lft. 2: astepl (Cos [--]a); astepr (Cos [--]y). 2: elim (H _ (compact_inc_lft _ _ Hab)); elim (H y X); intros. 2: inversion_clear X. 2: apply Cos_resp_leEq; auto. 2: astepl ( [--]ZeroR); apply less_leEq; apply inv_resp_less; auto. 2: apply less_leEq; apply less_transitive_unfolded with (Pi [/]TwoNZ). 2: astepr ( [--][--] (Pi [/]TwoNZ)); apply inv_resp_less; auto. 2: PiSolve. 2: apply inv_resp_leEq; auto. eapply leEq_transitive. apply Min_leEq_rht. apply leEq_wdr with (([1][/] _[//]Hsqrt) [*] (Cos (y[+]Pi [/]FourNZ) [+]Sin (y[+]Pi [/]FourNZ))). apply shift_div_leEq; auto. rstepr (Cos (y[+]Pi [/]FourNZ) [+]Sin (y[+]Pi [/]FourNZ)). set (z := y[+]Pi [/]FourNZ) in *. cut ([0] [<] z); intros. 2: unfold z in |- *; apply shift_less_plus. 2: astepl ( [--] (Pi [/]FourNZ)); auto. cut (z [<] Pi [/]TwoNZ); intros. 2: unfold z in |- *; apply shift_plus_less. 2: rstepr (Pi [/]FourNZ); auto. apply power_cancel_leEq with 2. auto. astepl (ZeroR[+][0]); apply plus_resp_leEq_both. apply less_leEq; apply pos_cos; try apply less_leEq; auto. apply less_leEq; apply Sin_pos; try apply less_leEq; auto. apply less_transitive_unfolded with (Pi [/]TwoNZ); PiSolve. simpl in |- *. astepl ([1][*]OneR); astepl OneR. apply leEq_wdr with (Cos z[^]2[+]Sin z[^]2[+]Two[*]Sin z[*]Cos z). 2: simpl in |- *; rational. astepr ([1][+]Sin (Two[*]z)). astepl ([1][+]ZeroR); apply less_leEq. apply plus_resp_leEq_less. apply leEq_reflexive. apply Sin_pos. apply shift_less_mult' with (two_ap_zero IR). apply pos_two. astepl ZeroR; auto. astepl (z[*]Two). apply shift_mult_less with (two_ap_zero IR). apply pos_two. auto. apply eq_transitive_unfolded with (Cos (y[+]Pi [/]FourNZ[+][--] (Pi [/]FourNZ))). 2: apply Cos_wd; rational. astepl (([1][/] _[//]Hsqrt) [*]Cos (y[+]Pi [/]FourNZ) [+] ([1][/] _[//]Hsqrt) [*]Sin (y[+]Pi [/]FourNZ)). astepl (Cos (Pi [/]FourNZ) [*]Cos (y[+]Pi [/]FourNZ) [+] Sin (Pi [/]FourNZ) [*]Sin (y[+]Pi [/]FourNZ)). astepl (Cos (Pi [/]FourNZ) [*]Cos (y[+]Pi [/]FourNZ) [+] [--][--] (Sin (Pi [/]FourNZ) [*]Sin (y[+]Pi [/]FourNZ))). astepl (Cos [--] (Pi [/]FourNZ) [*]Cos (y[+]Pi [/]FourNZ) [+] [--] ( [--] (Sin (Pi [/]FourNZ)) [*]Sin (y[+]Pi [/]FourNZ))). astepl (Cos [--] (Pi [/]FourNZ) [*]Cos (y[+]Pi [/]FourNZ) [+] [--] (Sin [--] (Pi [/]FourNZ) [*]Sin (y[+]Pi [/]FourNZ))). astepl (Cos [--] (Pi [/]FourNZ) [*]Cos (y[+]Pi [/]FourNZ) [-] Sin [--] (Pi [/]FourNZ) [*]Sin (y[+]Pi [/]FourNZ)). astepl (Cos (y[+]Pi [/]FourNZ) [*]Cos [--] (Pi [/]FourNZ) [-] Sin (y[+]Pi [/]FourNZ) [*]Sin [--] (Pi [/]FourNZ)). apply eq_symmetric_unfolded; apply Cos_plus. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac