proposition: Theorem summation_split_first : ∀ g b k, b ≤ k → Σ (i = b, k), g i = (g b + Σ (i = S b, k), g i)%K.
proof: Proof. intros g b k Hbk. unfold summation. rewrite Nat.sub_succ. rewrite <- summation_aux_succ_first. rewrite <- Nat.sub_succ_l; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc Field2