proposition: Lemma nth_rcons_cat_find x0 p s1 s2 x (s := rcons s1 x ++ s2) : p x -> ~~ has p s1 -> nth x0 s (find p s) = x.
proof: Proof. move=> pz pNs1; rewrite /s cat_rcons find_cat (negPf pNs1). by rewrite nth_cat/= pz addn0 subnn ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)