proposition: Lemma sorted_nfun_batcher m (t : (`2^ m).-tuple bool) : sorted <=%O (nfun (batcher m) t).
proof: Proof. elim: m t => [t|m IH t] /=; first by apply: tsorted01. rewrite nfun_cat. apply: sorted_nfun_batcher_merge_rec. by rewrite nfun_dup ttakeK; apply: IH. by rewrite nfun_dup; rewrite tdropK; apply: IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort