proposition: Lemma Abs_Sin_less_One : forall x, [--] (Pi [/]TwoNZ) [<] x -> x [<] Pi [/]TwoNZ -> AbsIR (Sin x) [<] [1].
proof: Proof. intros. apply power_cancel_less with 2. apply less_leEq; apply pos_one. astepr OneR. astepr (Cos x[^]2[+]Sin x[^]2). apply less_wdl with (Sin x[^]2). astepl ([0][+]Sin x[^]2). apply plus_resp_less_rht. apply pos_square. apply Greater_imp_ap; apply Cos_pos; auto. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply AbsIR_eq_x; apply sqr_nonneg. apply eq_symmetric_unfolded; apply AbsIR_nexp_op. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac