proposition: Lemma findP : find_spec (has a s) (find a s).
proof: Proof. have [a_s|aNs] := boolP (has a s); last by rewrite hasNfind//; constructor. by constructor=> [|x0|x0]; rewrite -?has_find ?nth_find//; apply: before_find. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)