proposition: Theorem apply_lap_inject_K_in_Kx_monom : ∀ P c, (@apply_lap _ (ps_ring K) (lap_inject_K_in_Kx P) (ps_monom c 0) = ps_monom (apply_lap P c) 0)%ps.
proof: Proof. intros P c. unfold apply_lap; simpl. unfold lap_inject_K_in_Kx. rename c into d. rewrite list_fold_right_map. induction P as [| a]; simpl. rewrite ps_zero_monom_eq; reflexivity. rewrite IHP. rewrite ps_monom_add_l, ps_monom_mul_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m