proposition: Lemma Sin_nonneg : forall x, [0] [<=] x -> x [<=] Pi -> [0] [<=] Sin x.
proof: Proof. simpl in |- *. intros; apply olor_pos_clcr_nonneg with ZeroR Pi I I. PiSolve. intros x0 H1 Hx; inversion_clear H1. apply less_wdr with (Sin x0); [ apply Sin_pos; auto | simpl in |- *; algebra ]. fold (Sin [0]) in |- *; apply eq_imp_leEq; algebra. fold (Sin Pi) in |- *; apply eq_imp_leEq; algebra. split; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac