proposition: Lemma Tan_pos : forall x, [0] [<] x -> x [<] Pi [/]TwoNZ -> forall Hx, [0] [<] Tan x Hx.
proof: Proof. intros. unfold Tan, Tang in |- *; simpl in |- *. apply shift_less_div. apply less_wdr with (Cos x). apply Cos_pos; auto. apply less_transitive_unfolded with ZeroR; PiSolve. simpl in |- *; algebra. astepl ZeroR; apply less_wdr with (Sin x). apply Sin_pos; auto. apply less_transitive_unfolded with (Pi [/]TwoNZ); PiSolve. simpl in |- *; algebra. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac