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