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