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