fact: Fixpoint knuth_exchange m : network (`2^ m) := if m is m1.+1 then neodup (knuth_exchange m1) ++ ceswap :: knuth_jump_rec _ m1 ((`2^ m1).-1) else [::].
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort