proposition: Theorem summation_aux_mul_swap : ∀ a g b len, (summation_aux r b len (λ i, a * g i) = a * summation_aux r b len g)%K.
proof: Proof. intros a g b len; revert b. induction len; intros; simpl. rewrite rng_mul_0_r; reflexivity. rewrite IHlen, rng_mul_add_distr_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2