proposition: Lemma cos_sin_Rabs : forall x, Rabs (cos x) = sqrt(1 - (sin x)²).
proof: Proof. intros x. unfold Rabs. destruct (Rcase_abs (cos x)). - rewrite <- (Ropp_involutive (sqrt (1 - (sin x)²))). apply Ropp_eq_compat. apply cos_sin_opp; lra. - apply cos_sin; assumption. Qed.
imports: Rbase Rtrigo1 Rfunctions Lra Ranalysis_reg