proposition: Lemma Has_cat (s1 s2 : seq T) : Has (s1 ++ s2) <-> Has s1 \/ Has s2.
proof: Proof. split. - by move/HasP=>[x] /Mem_cat; case=>Hx Px; [left|right]; apply/HasP; exists x. by case=>/HasP [x Hx Px]; apply/HasP; exists x=>//; apply/Mem_cat; [left|right]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)