proposition: Theorem apply_lap_add : ∀ α (r : ring α) la lb x, (apply_lap (lap_add la lb) x = apply_lap la x + apply_lap lb x)%K.
proof: Proof. intros α r la lb x. revert lb x. induction la as [| a]; intros; simpl. rewrite rng_add_0_l; reflexivity. destruct lb as [| b]; simpl. rewrite rng_add_0_r; reflexivity. rewrite IHla. do 2 rewrite rng_add_assoc. apply rng_add_compat_r. rewrite rng_add_shuffle0. rewrite rng_mul_add_distr_r; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn