proposition: Lemma tan_sin_opp : forall x, 0 > cos x -> tan x = - (sin x / sqrt (1 - (sin x)²)).
proof: Proof. intros x H. unfold tan. rewrite cos_sin_opp by lra. apply Rdiv_opp_r. Qed.
imports: Rbase Rtrigo1 Rfunctions Lra Ranalysis_reg