proposition: Lemma sorted_nfun_knuth_exchange m (t : (`2^ m).-tuple bool) : sorted <=%O (nfun (knuth_exchange m) t).
proof: Proof. elim: m t => [t|m IH t] /=; first by apply: tsorted01. rewrite nfun_cat /= nfun_eodup. set v := teocat _ _; have [||ste sto nto] := (@sorted_eswap _ v). - by rewrite tetakeK IH. - by rewrite totakeK IH. apply: sorted_knuth_jump_rec => //. rewrite nto andTb. rewrite -[X in _ <= _ + X](size_tuple (tetake (cfun ceswap v))). by rewrite -size_noFT addnCA leq_addr. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort