proposition: Lemma nat_ns_tail : forall p n, exists l, nat_ns p n = l ++ [:: p].
proof: Proof. move=> p; elim=> [|n [l' Ihn]] /=. - by exists [::]; rewrite cat0s. - rewrite Ihn. eexists. rewrite -cat_cons. reflexivity. Qed.
imports: ZArith Zwf Lia mathcomp(ssreflect eqtype ssrbool ssrnat div fintype seq ssrfun order) mathcomp(bigop fingroup choice ssralg ssrnum rat poly) pol