proposition: Theorem lap_eq_map_ext : ∀ α (r : ring α) A g h, (∀ a : A, (g a = h a)%K) → ∀ la : list A, (List.map g la = List.map h la)%lap.
proof: Proof. intros α r A g h Hgh la. induction la as [| a]; [ reflexivity | simpl ]. constructor; [ apply Hgh | assumption ]. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn