proposition: Lemma size_knuth_exchange m : size (knuth_exchange m) = (m * m.+1)./2.
proof: Proof. elim: m => // m IH. rewrite [LHS]/= size_cat /neodup /neomerge size_map size_zip minnn IH. rewrite [LHS]/= size_knuth_jump_rec -addn2 mulnDr halfD. by rewrite oddM muln2 odd_double andbF add0n doubleK mulnC. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort