proposition: Lemma Cos_pos : forall x, [--] (Pi [/]TwoNZ) [<] x -> x [<] Pi [/]TwoNZ -> [0] [<] Cos x.
proof: Proof. intros x H H0. assert (H1 : Continuous_I (less_leEq _ _ _ (less_transitive_unfolded _ _ _ _ H H0)) Cosine). apply included_imp_Continuous with realline; Contin. elim (contin_prop _ _ _ _ H1 Half (pos_half _)); intros d H2 H3. elim (less_cotransitive_unfolded _ _ _ H2 x); intros. apply pos_cos; try apply less_leEq; auto. assert (H4 : [--]d [<] [0]). astepr ( [--]ZeroR); apply inv_resp_less; auto. elim (less_cotransitive_unfolded _ _ _ H4 x); intros. 2: astepr (Cos [--]x); apply pos_cos. 2: astepl ( [--]ZeroR); apply inv_resp_leEq; apply less_leEq; auto. 2: apply inv_cancel_less; astepr x; auto. clear H4 H2 H1. astepl (OneR[-][1]). apply shift_minus_less; apply shift_less_plus'. apply leEq_less_trans with (Half:IR). 2: apply half_lt1. astepl (Cos [0][-]Cos x). eapply leEq_transitive. apply leEq_AbsIR. simpl in |- *; apply H3. split; PiSolve. split; apply less_leEq; auto. apply less_leEq; simpl in |- *; unfold ABSIR in |- *. apply Max_less. apply shift_minus_less; apply shift_less_plus'. astepl ( [--]d); auto. rstepl x; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac