proposition: Theorem summation_summation_exch : ∀ g k, (Σ (j = 0, k), Σ (i = 0, j), g i j = Σ (i = 0, k), Σ (j = i, k), g i j)%K.
proof: Proof. intros g k. induction k; [ reflexivity | idtac ]. rewrite summation_split_last; [ idtac | apply Nat.le_0_l ]. rewrite summation_split_last; [ idtac | apply Nat.le_0_l ]. rewrite summation_split_last; [ idtac | apply Nat.le_0_l ]. rewrite IHk. rewrite summation_only_one. rewrite rng_add_assoc. apply rng_add_compat_r. rewrite <- summation_add_distr. apply summation_compat; intros i (_, Hi). rewrite summation_split_last; [ reflexivity | idtac ]. apply Nat.le_le_succ_r; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2