proposition: Theorem apply_lap_mul : ∀ α (r : ring α) la lb x, (apply_lap (lap_mul 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 lap_mul_nil_l, rng_mul_0_l; reflexivity. destruct lb as [| b]; simpl. rewrite lap_mul_nil_r, rng_mul_0_r; reflexivity. rewrite lap_mul_cons; simpl. rewrite apply_lap_add; simpl. rewrite rng_add_0_r. rewrite apply_lap_add. rewrite IHla. rewrite IHla. simpl. rewrite rng_mul_0_l, rng_add_0_l. do 3 rewrite rng_mul_add_distr_r. do 2 rewrite rng_mul_add_distr_l. do 2 rewrite rng_mul_assoc. rewrite rng_add_assoc. apply rng_add_compat_r. rewrite rng_add_comm, rng_add_assoc. do 2 rewrite <- rng_add_assoc. apply rng_add_compat. apply rng_mul_compat_r. apply rng_mul_shuffle0. apply rng_add_compat. apply rng_mul_shuffle0. apply rng_mul_compat_r. apply apply_lap_single. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn