proposition: Theorem sigma_first : forall low high:nat, (low < high)%nat -> sigma low high = f low + sigma (S low) high.
proof: Proof. intros low high H1; generalize (proj2 (Nat.le_succ_l low high) H1); intro H2; generalize (Nat.lt_le_incl low high H1); intro H3; replace (f low) with (sigma low low). - apply sigma_split. + apply le_n. + assumption. - unfold sigma; rewrite Nat.sub_diag. simpl. replace (low + 0)%nat with low; [ reflexivity | ring ]. Qed.
imports: Rbase Rfunctions Rseries PartSum Lia