proposition: Lemma rem_filter s : uniq s -> rem s = filter (predC1 x) s.
proof: Proof. elim: s => //= y s IHs /andP[not_s_y /IHs->]. by case: eqP => //= <-; apply/esym/all_filterP; rewrite all_predC has_pred1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)