proposition: Lemma sorted_bool_constr m (s : seq bool) : sorted <=%O (s ++ (nseq m true)) = sorted <=%O s.
proof: Proof. elim: s => [|[] s IH]. - by case: m => // m; rewrite [nseq _.+1 _]/= isorted_consT size_nseq eqxx. - rewrite [(_ :: _) ++ _]/= !isorted_consT size_cat nseqD size_nseq. by rewrite eqseq_cat ?eqxx ?andbT ?size_nseq. by rewrite [(_ :: _) ++ _]/= !isorted_consF. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)