proposition: Theorem eq_series_trans {α} {r : ring α} : transitive _ eq_series.
proof: Proof. intros s₁ s₂ s₃ H₁ H₂. inversion H₁; inversion H₂; subst. constructor. etransitivity; [ apply H | apply H2 ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation