proposition: Lemma sin_asin : forall x, -1 <= x <= 1 -> sin (asin x) = x.
proof: Proof. intros x. unfold asin; repeat case Rle_dec. - rewrite sin_antisym, sin_PI2; lra. - rewrite sin_PI2; lra. - intros Hx1 Hx2 Hx3. pose proof Rsqr_bounds_lt 1 x ltac:(lra) as Hxsqr; rewrite Rsqr_1 in Hxsqr. rewrite sin_atan. unfold Rdiv at 1 2. rewrite Rmult_assoc, <- Rinv_mult. rewrite <- sqrt_mult_alt by lra. rewrite Rsqr_div', Rsqr_sqrt by lra. field_simplify ((1 - x²) * (1 + x² / (1 - x²))). { rewrite sqrt_1. field. } lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia