proposition: Theorem summation_ub_add : ∀ g k₁ k₂, (Σ (i = 0, k₁ + k₂), g i = Σ (i = 0, k₁), g i + Σ (i = S k₁, k₁ + k₂), g i)%K.
proof: Proof. intros g k₁ k₂. unfold summation. do 2 rewrite Nat.sub_0_r. rewrite <- Nat.add_succ_l. rewrite summation_aux_ub_add; simpl. rewrite Nat.add_comm, Nat.add_sub; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2