proposition: Lemma ns_step : forall p n, forall l1 l2 x y, 0 <= n -> ns p n = l1 ++ [:: x, y & l2] -> y = x + 1.
proof: Proof. move=> p [|n|n] /=; last 1 first. - by move=> ? ? ? ? /leb_Zneg0N. - move=> ? ? ? ? ?. by move/(congr1 size)=> /=; rewrite size_cat /= !addnS; move/eqP; rewrite eqSS. - move=> l1 l2 x y _; exact: nat_ns_step. Qed.
imports: ZArith Zwf Lia mathcomp(ssreflect eqtype ssrbool ssrnat div fintype seq ssrfun order) mathcomp(bigop fingroup choice ssralg ssrnum rat poly) pol