proposition: Lemma rem_mem y s : y != x -> y \in s -> y \in rem s.
proof: Proof. move=> yx; elim: s => [//|z s IHs] /=. rewrite inE => /orP[/eqP<-|ys]; first by rewrite (negbTE yx) inE eqxx. by case: ifP => _ //; rewrite inE IHs ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)