proposition: Theorem summation_add_distr : ∀ g h b k, (Σ (i = b, k), (g i + h i) = Σ (i = b, k), g i + Σ (i = b, k), h i)%K.
proof: Proof. intros g h b k. destruct (le_dec b k) as [Hbk| Hbk]. revert b Hbk. induction k; intros. destruct b. do 3 rewrite summation_only_one; reflexivity. unfold summation; simpl; rewrite rng_add_0_r; reflexivity. rewrite summation_split_last; [ idtac | assumption ]. rewrite summation_split_last; [ idtac | assumption ]. rewrite summation_split_last; [ idtac | assumption ]. destruct (eq_nat_dec b (S k)) as [H₂| H₂]. subst b. unfold summation; simpl. rewrite Nat.sub_diag; simpl. do 2 rewrite rng_add_0_l; rewrite rng_add_0_l. reflexivity. apply Nat_le_neq_lt in Hbk; [ idtac | assumption ]. apply Nat.succ_le_mono in Hbk. rewrite IHk; [ idtac | assumption ]. do 2 rewrite <- rng_add_assoc. apply rng_add_compat_l. rewrite rng_add_comm. rewrite <- rng_add_assoc. apply rng_add_compat_l. rewrite rng_add_comm. reflexivity. unfold summation. apply Nat.nle_gt in Hbk. replace (S k - b) with O by fast_omega Hbk; simpl. rewrite rng_add_0_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2