proposition: Lemma perm_iknuth_exchange_aux k p q (s : seq A) : perm_eq (iknuth_exchange_aux k p q s) s.
proof: Proof. elim: k p q s => //= k IH p q s. case: leqP => // q_gt0. apply: perm_trans; first by apply: IH. apply: perm_trans; first by apply: perm_iter3. by apply: perm_iter1. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort