proposition: Theorem sigma_eq_arg : forall low:nat, sigma low low = f low.
proof: Proof. intro; unfold sigma; rewrite Nat.sub_diag. simpl; replace (low + 0)%nat with low; [ reflexivity | ring ]. Qed.
imports: Rbase Rfunctions Rseries PartSum Lia