proposition: Lemma HalfPi_gt_pi_seq : forall n : nat, pi_seq n [<] Pi [/]TwoNZ.
proof: Proof. intros. unfold Pi in |- *. rstepr (Lim (Build_CauchySeq _ _ pi_seq_Cauchy)). apply less_leEq_trans with (pi_seq (S n)). apply pi_seq_incr. apply str_leEq_seq_so_leEq_Lim. exists (S n); intros. apply local_mon_imp_mon'. apply pi_seq_incr. auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos