proposition: Theorem lap_mul_const_l : ∀ α (r : ring α) a lb, lap_eq (lap_mul [a] lb) (List.map (rng_mul a) lb).
proof: Proof. intros α r a lb. unfold lap_mul; simpl. induction lb as [| b]; [ reflexivity | simpl ]. rewrite summation_only_one. constructor; [ reflexivity | idtac ]. rewrite lap_convol_mul_cons_succ; assumption. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn