proposition: Theorem list_nth_mod_div_deg_1 : ∀ la c i, (List.nth i (lap_mod_div_deg_1 R la c) 0 = apply_lap (List.skipn i la) c)%K.
proof: Proof. intros la c i; revert i. induction la as [| a]; intros; simpl. rewrite match_id, list_skipn_nil; reflexivity. destruct i; [ reflexivity | apply IHla ]. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn