proposition: Lemma Rabs_null_rev : forall r, Rabs r = 0 -> r = 0.
proof: Proof. intros r Hr ; destruct (Req_dec r 0) as [r_eq | r_neq]. assumption. destruct (Rabs_no_R0 _ r_neq Hr). Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR