proposition: Theorem all_0_summation_aux_0 : ∀ g b len, (∀ i, (b ≤ i < b + len) → (g i = 0)%K) → (summation_aux r b len (λ i, g i) = 0)%K.
proof: Proof. intros g b len H. revert b H. induction len; intros; [ reflexivity | simpl ]. rewrite H; [ idtac | split; auto ]. rewrite rng_add_0_l, IHlen; [ reflexivity | idtac ]. intros i (Hbi, Hib); apply H. rewrite Nat.add_succ_r, <- Nat.add_succ_l. split; [ apply Nat.lt_le_incl; auto | auto ]. rewrite Nat.add_succ_r. apply le_n_S, le_plus_l. Qed.
imports: Utf8 QArith NPeano Misc Field2