proposition: Lemma hasS (T : eqType) (p : pred T) s : has p s -> {a : T | a \in s & p a}.
proof: Proof. case: s => // b s H. pose a := (nth b (b :: s) (find p (b :: s))). exists a ; by rewrite ?mem_nth -?has_find ?nth_find. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)