proposition: Theorem ps_lap_nth_x_gt_pow_mul : ∀ la m n, (m < n)%nat → (ps_lap_nth m ([0; 1 … []] ^ n * la) = 0)%ps.
proof: Proof. intros la m n Hmn. revert m Hmn. induction n; intros. exfalso; revert Hmn; apply Nat.nlt_0_r. unfold ps_lap_mul, ps_lap_pow; simpl. 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; [ reflexivity | idtac ]. apply lt_S_n in Hmn. unfold ps_lap_nth; simpl. 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