proposition: Lemma Rabs_div : forall x y, y <> 0 -> Rabs (x / y) = Rabs x / Rabs y.
proof: Proof. intros x y H. unfold Rdiv. rewrite Rabs_mult. rewrite Rabs_Rinv. field. apply Rabs_no_R0. assumption. intuition. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra