proposition: Lemma Cos_one_gt_0 : [0] [<] Cos [1].
proof: Proof. apply cos_pi_seq_pos with (1%nat). apply less_leEq. apply pos_one. unfold pi_seq. rewrite -> Cos_zero. apply eq_imp_leEq. rational. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos