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