proposition: Lemma Sin_less_One : forall x : IR, [0] [<] Cos x -> Sin x [<] [1].
proof: Proof. intros. apply power_cancel_less with 2. auto. apply less_leEq; apply pos_one. astepr OneR. eapply less_wdr. 2: apply (FFT x). apply shift_less_plus. astepl ZeroR. apply pos_square; apply Greater_imp_ap; auto. Qed.
imports: CoRN.transc.Trigonometric