proposition: Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s).
proof: Proof. move=> xs; rewrite remE -[X in perm_eq X](cat_take_drop (index x s)). by rewrite drop_index// -cat1s perm_catCA cat1s. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)