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