proposition: Lemma size_batcher m : size (batcher m) = (m * m.+1)./2.
proof: Proof. elim: m => [//|m IH]. rewrite [in LHS]/= size_cat size_map size_zip minnn. rewrite size_batcher_merge_rec_aux IH. by rewrite -addn2 mulnDr -!divn2 divnDMl // mulnC. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort