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