proposition: Theorem lap_fold_compat_l : ∀ A (g h : A → _) la lb l, lap_eq la lb → lap_eq (List.fold_right (λ v accu, lap_add accu (lap_mul (g v) (h v))) la l) (List.fold_right (λ v accu, lap_add accu (lap_mul (g v) (h v))) lb l).
proof: Proof. intros A g h la lb l Heq. induction l; [ assumption | simpl; rewrite IHl; reflexivity ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation