proposition: Lemma sorted_iknuth_exchange (s : seq bool) : sorted <=%O (iknuth_exchange s).
proof: Proof. case: (ltP 3 (size s)) => [sl_gt4|]; last first. case: s => // a [|b [|c []]]//= _; lia. have ss_gt1 : 1 < size s by apply: leq_trans sl_gt4. have up_gt0 : 0 < up_log 2 (size s). by rewrite up_log_gt0 // (leq_trans _ sl_gt1). have up_gt1 : 1 < up_log 2 (size s). by rewrite -{1}[2]/(up_log 2 4) leq_up_log. apply: sorted_iknuth_exchange_aux => //. - by rewrite -ltnS prednK. - rewrite prednK //. by rewrite !e2nE; apply: up_log_bounds. - apply: ltn_trans (ltn_ne2n _) _. have /andP[] := (up_log_bounds (isT: 1 < 2) ss_gt1). by rewrite e2nE. move=> i iLu;rewrite prednK //. set x := up_log 2 _; split. have : size (eotake x i s) <= `2^ (x - x). apply: leq_size_eotake_e2n => //. by rewrite e2nE; apply: up_logP. by rewrite subnn; case: eotake => //= a [|]. have : size (eotake x (`2^ x.-1 + i) s) <= `2^ (x - x). apply: leq_size_eotake_e2n => //. by rewrite e2nE; apply: up_logP. by rewrite subnn; case: eotake => //= a [|]. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort