proposition: Theorem summation_aux_succ_last : ∀ g b len, (summation_aux r b (S len) g = summation_aux r b len g + g (b + len)%nat)%K.
proof: Proof. intros g b len. revert b. induction len; intros. simpl. rewrite rng_add_0_l, rng_add_0_r, Nat.add_0_r. reflexivity. remember (S len) as x; simpl; subst x. rewrite IHlen. simpl. rewrite rng_add_assoc, Nat.add_succ_r. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2