proposition: Lemma AbsIR_Sin_leEq_One : forall x : IR, AbsIR (Sin x) [<=] [1].
proof: Proof. intros. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_sqrt_sqr with (x2pos := sqr_nonneg _ (Sin x)). apply power_cancel_leEq with 2. auto with arith. apply less_leEq; apply pos_one. astepl (Sin x[^]2). astepr OneR. eapply leEq_wdr. 2: apply FFT with (x := x). apply shift_leEq_plus. astepl ZeroR. apply sqr_nonneg. Qed.
imports: CoRN.transc.Trigonometric