proposition: Theorem ps_lap_nth_x_le_pow_mul : ∀ la m n, (n ≤ m)%nat → (ps_lap_nth m ([0; 1 … []] ^ n * la) = ps_lap_nth (m - n) la)%ps.
proof: Proof. intros la m n Hnm. revert m Hnm. induction n; intros. progress unfold ps_lap_pow; simpl. progress unfold ps_lap_mul. rewrite lap_mul_1_l. rewrite Nat.sub_0_r. reflexivity. rewrite <- Nat.add_1_l. unfold ps_lap_pow. rewrite lap_power_add. rewrite lap_power_1. progress unfold ps_lap_mul. rewrite <- lap_mul_assoc. rewrite lap_mul_cons_l. rewrite lap_eq_0, lap_mul_nil_l, lap_add_nil_l, lap_mul_1_l. destruct m; [ exfalso; revert Hnm; apply Nat.nlt_0_r | simpl ]. apply le_S_n in Hnm. apply IHn; assumption. 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