proposition: Lemma pi_seq_gt_one : forall n : nat, [1] [<=] pi_seq (S n).
proof: Proof. intros. apply leEq_wdl with (pi_seq 1). 2: simpl in |- *. 2: Step_final (Cos [0]). apply local_mon_imp_mon'. intro; apply pi_seq_incr; auto. auto with arith. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos