proposition: Theorem lap_eq_list_fold_right : ∀ α (K : ring α) β g h x (l : list β), (∀ i a b, i ∈ l → lap_eq a b → lap_eq (g i a) (h i b)) → lap_eq (List.fold_right g x l) (List.fold_right h x l).
proof: Proof. intros α K β g h x l H. induction l as [| y]; intros; [ reflexivity | simpl ]. apply H; [ left; reflexivity | idtac ]. apply IHl; intros i a b Hi Heq. apply H; [ right; assumption | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation