proposition: Lemma sorted_rhalf_cleaner_rec m (t : (`2^ m.+1).-tuple bool) : sorted <=%O (ttake t : seq _) -> sorted <=%O (tdrop t : seq _) -> sorted <=%O (nfun (rhalf_cleaner_rec m.+1) t).
proof: Proof. rewrite /rhalf_cleaner_rec /= => Hst Hsd. rewrite nfun_dup. rewrite cfun_rhalf_cleaner_rev_drop -/e2n cfun_rhalf_cleaner_rev_take -/e2n. set u : (`2^ m.+1).-tuple _ := [tuple of _ ++ rev _]. have uB : (u : seq _) \is bitonic. apply: bitonic_cat => //. by rewrite rev_sorted. have := bitonic_half_cleaner false uB; rewrite -/e2n => /orP[/andP[Ht Hd]|/andP[Ht Hd]]. have -> : ttake (cfun (half_cleaner false (`2^ m)) u) = [tuple of nseq (`2^ m) false]. by apply/val_eqP. rewrite nfun_const sorted_bool_constl. apply: sorted_half_cleaner_rec. by rewrite bitonic_rev. have -> : trev (tdrop (cfun (half_cleaner false (`2^ m)) u)) = [tuple of nseq (`2^ m) true]. by apply/val_eqP; rewrite /= (eqP Ht) rev_nseq. rewrite nfun_const sorted_bool_constr. by apply: sorted_half_cleaner_rec. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort