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