proposition: Lemma Datan_continuity : continuity (fun x => /(1 + x^2)).
proof: Proof. apply continuity_inv. { apply continuity_plus. { apply continuity_const ; unfold constant ; intuition. } apply derivable_continuous ; apply derivable_pow. } intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|lra] ; apply Rplus_ge_compat_l. replace (x^2) with (x²). { apply Rle_ge ; apply Rle_0_sqr. } unfold Rsqr ; field. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia