proposition: Theorem ps_lap_nth_add : ∀ n la lb, (ps_lap_nth n (la + lb) = ps_lap_nth n la + ps_lap_nth n lb)%ps.
proof: Proof. intros n la lb. unfold ps_lap_add; simpl. unfold ps_lap_nth; simpl. revert n lb. induction la as [| a]; intros; simpl. rewrite match_id, ps_add_0_l; reflexivity. destruct lb as [| b]; simpl. rewrite match_id, ps_add_0_r; reflexivity. destruct n; [ reflexivity | apply IHla ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Puiseux_series Ps_add Ps_mul Ps_div