proposition: Lemma nat_ns_head : forall (p : Z) n, exists l, nat_ns p n = (p - (Z_of_nat n))%Z :: l.
proof: Proof. move=> p; elim=>[|n [l Ih]] /=. exists [::]. by rewrite Z.sub_0_r. by rewrite Ih; exists [:: (p - Z_of_nat n)%Z & l]. Qed.
imports: ZArith Zwf Lia mathcomp(ssreflect eqtype ssrbool ssrnat div fintype seq ssrfun order) mathcomp(bigop fingroup choice ssralg ssrnum rat poly) pol