proposition: Theorem summation_only_one_non_0 : ∀ g b v k, (b ≤ v ≤ k) → (∀ i, (b ≤ i ≤ k) → (i ≠ v) → (g i = 0)%K) → (Σ (i = b, k), g i = g v)%K.
proof: Proof. intros g b v k (Hbv, Hvk) Hi. unfold summation. rewrite Nat.sub_succ_l; [ idtac | etransitivity; eassumption ]. remember (k - b) as len. replace k with (b + len) in * . clear k Heqlen. revert b v Hbv Hvk Hi. induction len; intros. simpl. rewrite rng_add_0_r. replace b with v ; [ reflexivity | idtac ]. rewrite Nat.add_0_r in Hvk. apply Nat.le_antisymm; assumption. remember (S len) as x; simpl; subst x. destruct (eq_nat_dec b v) as [H₁| H₁]. subst b. rewrite all_0_summation_aux_0. rewrite rng_add_0_r; reflexivity. intros j (Hvj, Hjv). simpl in Hjv. apply le_S_n in Hjv. apply Hi; [ split; auto; apply Nat.lt_le_incl; auto | idtac ]. intros H; subst j. revert Hvj; apply Nat.nle_succ_diag_l. rewrite Nat.add_succ_r, <- Nat.add_succ_l in Hvk. rewrite Hi; auto. rewrite rng_add_0_l. apply IHlen; auto; [ apply Nat_le_neq_lt; auto | idtac ]. intros j (Hvj, Hjvl) Hjv. rewrite Nat.add_succ_l, <- Nat.add_succ_r in Hjvl. apply Hi; auto; split; auto. apply Nat.lt_le_incl; auto. split; auto. apply Nat.le_sub_le_add_l. rewrite Nat.sub_diag. apply Nat.le_0_l. subst len. eapply Nat.le_trans in Hvk; eauto . rewrite Nat.add_sub_assoc; auto. rewrite Nat.add_comm. apply Nat.add_sub. Qed.
imports: Utf8 QArith NPeano Misc Field2