proposition: Lemma sorted_bool_constl m (s : seq bool) : sorted <=%O ((nseq m false) ++ s) = sorted <=%O s.
proof: Proof. by elim: m => // [] n; rewrite [nseq _.+1 _ ++ _]/= isorted_consF. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)