proposition: Theorem summation_shift : ∀ b g k, b ≤ k → (Σ (i = b, k), g i = Σ (i = 0, k - b), g (b + i)%nat)%K.
proof: Proof. intros b g k Hbk. unfold summation. rewrite Nat.sub_0_r. rewrite Nat.sub_succ_l; [ idtac | assumption ]. apply summation_aux_compat; intros j Hj. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2