proposition: Theorem sigma_diff_neg : forall low high k:nat, (low <= k)%nat -> (k < high)%nat -> sigma low k - sigma low high = - sigma (S k) high.
proof: Proof. intros low high k H1 H2; rewrite (sigma_split H1 H2); ring. Qed.
imports: Rbase Rfunctions Rseries PartSum Lia