proposition: Lemma sin_cos_opp : forall x, sin x <=0 -> sin x = - sqrt(1 - (cos x)²).
proof: Proof. intros x H. rewrite <- (Ropp_involutive (sin x)). apply Ropp_eq_compat. apply Rsqr_inj. - lra. - apply sqrt_pos. - rewrite Rsqr_sqrt. + rewrite <- Rsqr_neg. apply sin2. + pose proof cos2_bound x. lra. Qed.
imports: Rbase Rtrigo1 Rfunctions Lra Ranalysis_reg