proposition: Theorem lap_inject_comp : ∀ la lb, (lap_inject_K_in_Kx la ∘ lap_inject_K_in_Kx lb = lap_inject_K_in_Kx (lap_compose la lb))%pslap.
proof: Proof. intros la lb. progress unfold lap_inject_K_in_Kx; simpl. progress unfold ps_lap_comp. progress unfold lap_compose. revert lb. induction la as [| a]; intros; [ reflexivity | simpl ]. rewrite IHla. do 3 rewrite fold_lap_inject_K_in_Kx. rewrite fold_ps_lap_mul. rewrite lap_inject_mul. rewrite <- lap_inject_add. 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