proposition: Lemma AbsIR_Sin_less_One : forall x : IR, [0] [<] Cos x -> AbsIR (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. apply less_wdl with ZeroR. apply pos_square; apply Greater_imp_ap; auto. apply eq_symmetric_unfolded; apply x_minus_x. eapply eq_transitive_unfolded. 2: apply AbsIR_eq_x. 2: apply sqr_nonneg. apply eq_symmetric_unfolded; apply AbsIR_nexp_op. Qed.
imports: CoRN.transc.Trigonometric