proposition: Lemma ns_head : forall p n :Z, (0 <= n) -> exists l, ns p n = (p - n) :: l.
proof: Proof. move=> p [|n|n] /=; last 1 first. - by move/leb_Zneg0N. - exists [::]. by rewrite Z.sub_0_r. - move=> _; set m := nat_of_P n; case: (nat_ns_head p m)=> l' ->; exists l'. by rewrite /m Zpos_eq_Z_of_nat_o_nat_of_P. Qed.
imports: ZArith Zwf Lia mathcomp(ssreflect eqtype ssrbool ssrnat div fintype seq ssrfun order) mathcomp(bigop fingroup choice ssralg ssrnum rat poly) pol