proposition: Lemma sorting_bfsort m : bfsort false m \is sorting.
proof: Proof. rewrite /sorting. rewrite -[<=%O]/(if false then (>=%O : rel _) else <=%O). elim: m false => [b|m IH b]; first by apply/forallP => /= [] [[|x[]]]. apply/forallP => t. rewrite /bfsort -/bfsort nfun_cat. apply: sorted_half_cleaner_rec. rewrite nfun_merge ?size_bfsort //. case: b; last first. apply: bitonic_cat; first by have /forallP := IH false; apply. by have /forallP := IH true; apply. apply: bitonic_catr; first by have /forallP := IH true; apply. by have /forallP := IH false; apply. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort