proposition: Lemma Sin_resp_less : forall x y, [--] (Pi [/]TwoNZ) [<=] x -> x [<] y -> y [<=] Pi [/]TwoNZ -> Sin x [<] Sin y.
proof: Proof. intros. astepl (Cos (Pi [/]TwoNZ[-]x)); astepr (Cos (Pi [/]TwoNZ[-]y)). apply Cos_resp_less; auto. apply shift_leEq_minus; astepl y; auto. unfold cg_minus in |- *; apply plus_resp_leEq_less; [ apply leEq_reflexive | apply inv_resp_less; auto ]. apply shift_minus_leEq; apply shift_leEq_plus'; rstepl ( [--] (Pi [/]TwoNZ)); auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac