proposition: Theorem summation_split_last : ∀ g b k, (b ≤ S k) → (Σ (i = b, S k), g i = Σ (i = b, k), g i + g (S k))%K.
proof: Proof. intros g b k Hbk. unfold summation. rewrite Nat.sub_succ_l; [ idtac | assumption ]. rewrite summation_aux_succ_last. rewrite Nat.add_sub_assoc; [ idtac | assumption ]. rewrite Nat.add_comm, Nat.add_sub. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2