proposition: Theorem lap_inject_add : ∀ la lb, (lap_inject_K_in_Kx la + lap_inject_K_in_Kx lb = lap_inject_K_in_Kx (la + lb)%lap)%pslap.
proof: Proof. intros la lb. unfold lap_inject_K_in_Kx. revert lb. induction la as [| a]; intros; simpl. progress unfold ps_lap_add. rewrite lap_add_nil_l; reflexivity. destruct lb as [| b]; simpl. progress unfold ps_lap_add. rewrite lap_add_nil_r; reflexivity. progress unfold ps_lap_add. rewrite lap_add_cons. constructor; [ simpl | apply IHla ]. rewrite ps_monom_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