proposition: Lemma tan_pi_minus : forall x, cos x <> 0 -> tan (PI - x) = - tan x.
proof: Proof. intros x H. unfold tan; rewrite sin_pi_minus, cos_pi_minus. field; assumption. Qed.
imports: Rbase Rtrigo1 Rfunctions Lra Ranalysis_reg