proposition: Lemma sorting_knuth_exchange m : knuth_exchange m \is sorting.
proof: Proof. apply/forallP => x; apply: sorted_nfun_knuth_exchange. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort