proposition: Lemma sorting_bsort m : bsort m \is sorting.
proof: Proof. elim: m => [|m IH]; first by apply: sorting1. apply/forallP => t. rewrite /bsort -/bsort nfun_cat. apply: sorted_rhalf_cleaner_rec; first by rewrite nfun_dup ttakeK (forallP IH). by rewrite nfun_dup tdropK (forallP IH). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort