proposition: Lemma size_swap (s : seq A) i j : i < j < size s -> size (swap i j s) = size s.
proof: Proof. by move=> jB; apply/perm_size/perm_swap. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort