proposition: Lemma cos_tan : forall x, 0 < cos x -> cos x = 1 / sqrt (1 + (tan x)²).
proof: Proof. intros. destruct (Rcase_abs (sin x)) as [Hsignsin|Hsignsin]. - assert(Hsinle:0>=sin x) by lra. pose proof tan_cos_opp x Hsinle as Htan. rewrite Htan. rewrite Rsqr_div'. rewrite <- Rsqr_neg. pose proof cos2_bound x. pose proof Rsqr_pos_lt (cos x) ltac:(lra). pose proof sqrt_lt_R0 (cos x)² ltac:(assumption). rewrite Rsqr_sqrt. 2:lra. field_simplify( 1 + (1 - (cos x)²) / (cos x)² ). 2:lra. rewrite sqrt_div_alt. 2:lra. rewrite sqrt_1. field_simplify_eq. 2:lra. rewrite sqrt_Rsqr;lra. - assert(Hsinge:0<=sin x) by lra. pose proof tan_cos x Hsinge as Htan. rewrite Htan. rewrite Rsqr_div'. pose proof cos2_bound x. pose proof Rsqr_pos_lt (cos x) ltac:(lra). pose proof sqrt_lt_R0 (cos x)² ltac:(assumption). rewrite Rsqr_sqrt. 2:lra. field_simplify( 1 + (1 - (cos x)²) / (cos x)² ). 2:lra. rewrite sqrt_div_alt. 2:lra. rewrite sqrt_1. field_simplify_eq. 2:lra. rewrite sqrt_Rsqr;lra. Qed.
imports: Rbase Rtrigo1 Rfunctions Lra Ranalysis_reg