proposition: Lemma Boule_lt : forall c r x, Boule c r x -> Rabs x < Rabs c + r.
proof: Proof. unfold Boule; intros c r x h. apply Rabs_def2 in h; destruct h; apply Rabs_def1; (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; lra | rewrite <- Rabs_Ropp, Rabs_pos_eq; lra]). Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia