proposition: Theorem eq_series_sym {α} {r : ring α} : symmetric _ eq_series.
proof: Proof. intros s₁ s₂ H. inversion H; subst. constructor. intros i; symmetry; apply H0. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation