proposition: Lemma sin_tan : forall x, 0 < cos x -> sin x = tan x / sqrt (1 + (tan x)²).
proof: Proof. intros. assert(Hcosle:0<=cos x) by lra. pose proof tan_sin x Hcosle as Htan. pose proof (sin2 x); pose proof Rsqr_pos_lt (cos x). rewrite Htan. unfold Rdiv at 1 2. rewrite Rmult_assoc, <- Rinv_mult. rewrite <- sqrt_mult_alt by lra. rewrite Rsqr_div', Rsqr_sqrt by lra. field_simplify ((1 - (sin x)²) * (1 + (sin x)² / (1 - (sin x)²))). - rewrite sqrt_1. field. - lra. Qed.
imports: Rbase Rtrigo1 Rfunctions Lra Ranalysis_reg