fact: Fixpoint iknuth_exchange_aux k top p (s : seq A) := if k is k1.+1 then if p > 0 then let l1 := iter3 top p (iter1 p s) in iknuth_exchange_aux k1 top p./2 l1 else s else s.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort