proposition: Theorem nth_mul_deg_1 : ∀ α (r : ring α) a lb k, (List.nth (S k) (lap_mul [a; 1 … []] lb) 0 = a * List.nth (S k) lb 0 + List.nth k lb 0)%K.
proof: Proof. intros α r a lb k. unfold lap_mul. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite summation_split_first; [ simpl | apply le_n_S, Nat.le_0_l ]. rewrite all_0_summation_0. rewrite rng_mul_1_l, Nat.sub_0_r, rng_add_0_r; reflexivity. intros i (Hi, Hik). destruct i; [ exfalso; revert Hi; apply Nat.nle_succ_0 | idtac ]. apply Nat.succ_le_mono in Hi. destruct i; [ exfalso; revert Hi; apply Nat.nle_succ_0 | idtac ]. rewrite match_id, rng_mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn