proposition: Theorem list_fold_right_compat : ∀ α β equal g h (a₀ : α) (l : list β), (∀ x y z, equal x y → equal (g z x) (h z y)) → equal a₀ a₀ → equal (List.fold_right g a₀ l) (List.fold_right h a₀ l).
proof: Proof. intros α β equal g h a₀ l Hcomp Heq. induction l as [| x]; intros; [ assumption | idtac ]. apply Hcomp; assumption. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol