proposition: Theorem summation_add_add_sub : ∀ g b k n, (Σ (i = b, k), g i = Σ (i = b + n, k + n), g (i - n)%nat)%K.
proof: Proof. intros g b k n. unfold summation. replace (S (k + n) - (b + n))%nat with (S k - b)%nat by fast_omega. apply summation_aux_compat. intros i Hi. replace (b + n + i - n)%nat with (b + i)%nat by fast_omega. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2