fact: Definition iknuth_exchange (s : seq A) : seq A := let top := `2^ ((up_log 2 (size s)).-1) in iknuth_exchange_aux (size s) top top s.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort