proposition: Theorem summation_aux_ub_add : ∀ g b k₁ k₂, (summation_aux r b (k₁ + k₂) g = summation_aux r b k₁ g + summation_aux r (b + k₁) k₂ g)%K.
proof: Proof. intros g b k₁ k₂. revert b k₁. induction k₂; intros. simpl. rewrite Nat.add_0_r, rng_add_0_r; reflexivity. rewrite Nat.add_succ_r, <- Nat.add_succ_l. rewrite IHk₂; simpl. rewrite <- Nat.add_succ_r. rewrite rng_add_assoc. apply rng_add_compat_r. clear k₂ IHk₂. revert b. induction k₁; intros; simpl. rewrite Nat.add_0_r. apply rng_add_comm. rewrite <- rng_add_assoc. rewrite IHk₁. rewrite Nat.add_succ_r, <- Nat.add_succ_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2