proposition: Lemma size_batcher_merge_rec_aux m : size (batcher_merge_rec_aux m) = m.+1.
proof: Proof. elim: m => [//| m IH] /=. by rewrite size_rcons size_map size_zip minnn IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort