proposition: Lemma exists_cons {P : T -> Prop} {a s} : (exists2 x, x \in a::s & P x) <-> P a \/ exists2 x, x \in s & P x.
proof: Proof. split=> [[x /predU1P[->|x_s] Px]|]; [by left| by right; exists x|]. by move=> [?|[x x_s ?]]; [exists a|exists x]; rewrite ?inE ?eqxx ?x_s ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)