proposition: Theorem all_0_summation_0 : ∀ g i₁ i₂, (∀ i, i₁ ≤ i ≤ i₂ → (g i = 0)%K) → (Σ (i = i₁, i₂), g i = 0)%K.
proof: Proof. intros g i₁ i₂ H. apply all_0_summation_aux_0. intros i (H₁, H₂). apply H. split; [ assumption | idtac ]. destruct (le_dec i₁ (S i₂)) as [H₃| H₃]. rewrite Nat.add_sub_assoc in H₂; auto. rewrite minus_plus in H₂. apply le_S_n; auto. apply not_le_minus_0 in H₃. rewrite H₃, Nat.add_0_r in H₂. apply Nat.nle_gt in H₂; contradiction. Qed.
imports: Utf8 QArith NPeano Misc Field2