proposition: Theorem summation_succ_succ : ∀ b k g, (Σ (i = S b, S k), g i = Σ (i = b, k), g (S i))%K.
proof: Proof. intros b k g. unfold summation. rewrite Nat.sub_succ. remember (S k - b)%nat as len; clear Heqlen. revert b. induction len; intros; [ reflexivity | simpl ]. rewrite IHlen; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2