proposition: Lemma sin_inj x y : -(PI/2) <= x <= PI/2 -> -(PI/2) <= y <= PI/2 -> sin x = sin y -> x = y.
proof: Proof. intros xP yP Hsin. destruct (total_order_T x y) as [[H|H]|H]; auto. - assert (sin x < sin y). + now apply sin_increasing_1; lra. + now lra. - assert (sin y < sin x). + now apply sin_increasing_1; lra. + now lra. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg