proposition: Lemma Pi_gt_2 : Two [<] Pi.
proof: Proof. unfold Pi. rstepl (Two [*] [1]:IR). apply mult_resp_less_lft. apply less_leEq_trans with ([1] [+] (Cos [1])). rstepl ([1] [+] [0]:IR). apply plus_resp_leEq_less. apply eq_imp_leEq. reflexivity. apply Cos_one_gt_0. apply str_leEq_seq_so_leEq_Lim. exists (2%nat). intros i iH. change ([1] [+] Cos [1][<=] pi_seq i). induction i. exfalso. auto with *. clear IHi. induction i. exfalso. auto with *. clear iH. clear IHi. induction i. unfold pi_seq. rewrite -> Cos_zero. setoid_replace ([0] [+] [1]:IR) with ([1]:IR); [|rational]. apply eq_imp_leEq. reflexivity. apply leEq_transitive with (pi_seq (S (S i))). assumption. apply less_leEq. apply pi_seq_incr. apply pos_two. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos