proposition: Lemma tan_inj : forall x y, -PI/2 < x < PI/2 -> -PI/2 < y < PI/2 -> tan x = tan y -> x = y.
proof: Proof. intros a b a_encad b_encad fa_eq_fb. destruct (total_order_T a b) as [[Hf|?]|Hf]. - assert (Hfalse := tan_increasing a b (proj1 a_encad) Hf (proj2 b_encad)). case (Rlt_not_eq (tan a) (tan b)) ; assumption. - intuition. - assert (Hfalse := tan_increasing b a (proj1 b_encad) Hf (proj2 a_encad)). case (Rlt_not_eq (tan b) (tan a)) ; [|symmetry] ; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia