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