proposition: Lemma Sin_pos : forall x : IR, [0] [<] x -> x [<] Pi -> [0] [<] Sin x.
proof: Proof. intros. astepr (Cos (Pi [/]TwoNZ[-]x)). apply Cos_pos. apply shift_less_minus; apply shift_plus_less'. unfold cg_minus in |- *; rstepr Pi; auto. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac