proposition: Theorem lap_mul_fold_add_distr : ∀ β la li (g : β → list α) x, lap_eq (lap_mul x (List.fold_right (λ i accu, lap_add accu (g i)) la li)) (List.fold_right (λ i accu, lap_add accu (lap_mul x (g i))) (lap_mul x la) li).
proof: Proof. intros uβ la li g x. revert la x. induction li as [| j]; intros; [ reflexivity | simpl ]. rewrite lap_mul_add_distr_l. rewrite IHli; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation