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