proposition: Lemma sorted_half_cleaner_rec b m (t : (`2^ m).-tuple bool) : (t : seq _) \is bitonic -> sorted (if b then (>=%O : rel _) else <=%O) (nfun (half_cleaner_rec b m) t).
proof: Proof. elim: m t b => /= [|m IH t b tB]; first by (do 2 case => //=) => x []. rewrite nfun_dup. have /orP[/andP[Ht Hd]|/andP[Ht Hd]] := bitonic_half_cleaner b tB. have -> : ttake (cfun (half_cleaner b (`2^ m)) t) = [tuple of nseq (`2^ m) b]. by apply/val_eqP. rewrite nfun_const. case: b Ht Hd => Ht Hd; last by rewrite sorted_bool_constl ; apply: IH. rewrite -rev_sorted rev_cat /= rev_nseq sorted_bool_constr rev_sorted /=. by apply: IH. have -> : tdrop (cfun (half_cleaner b (`2^ m)) t) = [tuple of nseq (`2^ m) (~~b)]. by apply/val_eqP. rewrite nfun_const. case: b Ht Hd => Ht Hd; last by rewrite sorted_bool_constr; apply: IH. rewrite -rev_sorted rev_cat /= rev_nseq sorted_bool_constl rev_sorted /=. by apply: IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort