proposition: Theorem inserted_0_summation : ∀ g h k n, n ≠ O → (∀ i, i mod n ≠ O → (g i = 0)%K) → (∀ i, (g (n * i)%nat = h i)%K) → (Σ (i = 0, k * n), g i = Σ (i = 0, k), h i)%K.
proof: Proof. intros g h k n Hn Hf Hfg. destruct k. rewrite Nat.mul_0_l. apply summation_compat; intros i (_, Hi). apply Nat.le_0_r in Hi; subst i. rewrite <- Hfg, Nat.mul_0_r; reflexivity. destruct n; [ exfalso; apply Hn; reflexivity | clear Hn ]. replace (S k * S n)%nat with (S k * S n - 1 + 1)%nat. rewrite summation_ub_add. rewrite summation_mul_summation_summation; try apply Nat.lt_0_succ. rewrite Nat_sub_succ_1, Nat.add_comm, summation_only_one. simpl; do 2 rewrite Nat.sub_0_r. symmetry. rewrite <- Nat.add_1_r, summation_ub_add, Nat.add_1_r. rewrite summation_only_one, rng_add_comm, <- Hfg. symmetry. rewrite rng_add_comm. apply rng_add_compat; [ symmetry; rewrite Nat.mul_comm; reflexivity | ]. apply summation_compat; intros i Hi. rewrite summation_only_one_non_0 with (v := 0). rewrite Nat.add_0_r, Nat.mul_comm; apply Hfg. split; [ reflexivity | apply Nat.le_0_l ]. intros j Hjn Hj. rewrite Hf; [ reflexivity | ]. rewrite Nat.add_comm. rewrite Nat.mod_add; [ | apply Nat.neq_succ_0 ]. intros H; apply Hj; clear Hj. apply Nat.mod_divides in H; auto. destruct H as (c, Hc). destruct c. rewrite Nat.mul_0_r in Hc; assumption. rewrite Hc in Hjn. rewrite Nat.mul_comm in Hjn. simpl in Hjn. destruct Hjn as (_, H). apply Nat.nlt_ge in H. exfalso; apply H. apply le_n_S, Nat.le_add_r. rewrite Nat.sub_add; [ apply eq_refl | ]. simpl; apply le_n_S, Nat.le_0_l. Qed.
imports: Utf8 QArith NPeano Misc Field2