proposition: Lemma sorted_nfun_batcher_merge m (t : (`2^ m.+1).-tuple bool) : sorted <=%O (ttake t) -> sorted <=%O (tdrop t) -> sorted <=%O (nfun (batcher_merge_rec m.+1) t).
proof: Proof. exact: sorted_nfun_batcher_merge_rec. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort