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