proposition: Lemma size_half_cleaner_rec b m : size (half_cleaner_rec b m) = m.
proof: Proof. elim: m => //= m IH. by rewrite /ndup /= size_map size_zip IH minnn. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort