proposition: Theorem lap_mul_map_ps : ∀ la lb, (List.map (λ c, ps_monom c 0) (la * lb)%lap = List.map (λ c, ps_monom c 0) la * List.map (λ c, ps_monom c 0) lb)%pslap.
proof: Proof. intros la lb. progress unfold ps_lap_eq, ps_lap_mul, lap_mul; simpl. do 2 rewrite List.map_length. remember (pred (length la + length lb)) as len. clear Heqlen. remember 0%nat as n; clear Heqn. revert n la lb. induction len; intros; [ reflexivity | simpl ]. constructor; [ simpl | apply IHlen ]. clear len IHlen; simpl. unfold summation. rewrite ps_monom_summation_aux. apply summation_compat; intros i (_, Hi); simpl. rewrite ps_monom_mul_l. rewrite rng_list_map_nth. rewrite rng_list_map_nth; [ reflexivity | idtac ]. rewrite ps_zero_monom_eq; reflexivity. rewrite ps_zero_monom_eq; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol