proposition: Lemma splitmn : forall n m, d n <> 0 -> d m <> 0 -> m <> n -> / ((d n) * (d m)) = / (2 * (m - n)) * (/ (d n) - / (d m)).
proof: Proof. intros. unfold d in *. field. split; [|split]. assumption. assumption. apply Rminus_eq_contra; assumption. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith