proposition: Theorem rng_list_map_nth : ∀ A n f l (d : A) fd, (fd = f d)%K → (List.nth n (List.map f l) fd = f (List.nth n l d))%K.
proof: Proof. intros A n f l d fd Hfd. revert n d fd Hfd. induction l as [| x]; intros; simpl. destruct n; assumption. destruct n; [ reflexivity | idtac ]. apply IHl; 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