proposition: Theorem lap_eq_nil_nth : ∀ la, lap_eq la [] → ∀ n, (List.nth n la 0 = 0)%K.
proof: Proof. intros la H n. revert n. induction la as [| a]; intros; simpl. rewrite match_id; reflexivity. apply lap_eq_cons_nil_inv in H. destruct H as (Ha, Hla). destruct n; [ assumption | idtac ]. apply IHla; assumption. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn