proposition: Lemma nth_cat_seqT a b i : nth true (nseq a false ++ nseq b true) i = (a <= i).
proof: Proof. by rewrite nth_cat !nth_nseq !size_nseq if_same; case: leqP. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)