proposition: Lemma size_batcher_merge_rec m : size (batcher_merge_rec m) = m.
proof: Proof. by case: m => //= m; rewrite size_batcher_merge_rec_aux. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort