proposition: Theorem series_add_assoc : ∀ s₁ s₂ s₃, (s₁ + (s₂ + s₃) = (s₁ + s₂) + s₃)%ser.
proof: Proof. intros s₁ s₂ s₃. unfold series_add; simpl. constructor; intros i; simpl. rewrite rng_add_assoc; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation