proposition: Lemma pos_cos : forall x, [0] [<=] x -> x [<] Pi [/]TwoNZ -> [0] [<] Cos x.
proof: Proof. intros x H H0. assert (H1 : x [<] Lim (Build_CauchySeq _ _ pi_seq_Cauchy)). apply less_wdr with (Pi [/]TwoNZ); auto; unfold Pi in |- *; rational. elim (less_Lim_so_less_seq _ _ H1); intros N HN. apply cos_pi_seq_pos with N. auto. apply less_leEq; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos