proposition: Lemma size_iknuth_exchange_aux k p q (s : seq A) : size (iknuth_exchange_aux k p q s) = size s.
proof: Proof. by apply/perm_size/perm_iknuth_exchange_aux. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort