proposition: Theorem apply_lap_single : ∀ α (r : ring α) a lb x, (apply_lap (lap_mul [a] lb) x = a * apply_lap lb x)%K.
proof: Proof. intros α r a lb x. induction lb as [| b]. simpl; rewrite rng_mul_0_r; reflexivity. rewrite lap_mul_cons_r; simpl. rewrite summation_only_one, rng_add_0_r, IHlb. rewrite rng_mul_add_distr_l, rng_mul_assoc; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn