proposition: Theorem lap_add_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. apply lap_add_map; intros a b. rewrite ps_monom_add_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Puiseux_series Ps_add Ps_mul Ps_div