proposition: Theorem lap_inject_mul : ∀ 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_mul. do 2 rewrite lap_mul_nil_l; reflexivity. destruct lb as [| b]; simpl. progress unfold ps_lap_mul. do 2 rewrite lap_mul_nil_r; reflexivity. progress unfold ps_lap_mul. do 2 rewrite lap_mul_cons; simpl. constructor; [ simpl; apply ps_monom_mul | idtac ]. symmetry. eapply ps_lap_eq_trans; [ apply lap_add_map_ps | ]. unfold ps_lap_mul in IHla. unfold ps_lap_eq in IHla. rewrite IHla. progress unfold ps_lap_add. simpl. rewrite ps_zero_monom_eq. apply lap_add_compat; [ idtac | reflexivity ]. eapply ps_lap_eq_trans; [ apply lap_add_map_ps | ]. apply lap_add_compat. eapply ps_lap_eq_trans; [ apply lap_mul_map_ps | reflexivity ]. eapply ps_lap_eq_trans; [ apply lap_mul_map_ps | 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