proposition: Theorem apply_lap_compose : ∀ α (r : ring α) la lb x, (apply_lap (lap_compose la lb) x = apply_lap la (apply_lap lb x))%K.
proof: Proof. intros α r la lb x. unfold lap_compose. revert lb x. induction la as [| a]; intros; [ reflexivity | simpl ]. rewrite <- IHla; clear. rewrite apply_lap_add; simpl. rewrite rng_mul_0_l, rng_add_0_l. apply rng_add_compat_r. apply apply_lap_mul. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn