proposition: Lemma cos_inj x y : 0 <= x <= PI -> 0 <= y <= PI -> cos x = cos y -> x = y.
proof: Proof. intros xP yP Hcos. destruct (total_order_T x y) as [[H|H]|H]; auto. - assert (cos y < cos x). + now apply cos_decreasing_1; lra. + now lra. - assert (cos x < cos y). + now apply cos_decreasing_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