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