proposition: Lemma find_cat s1 s2 : find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.
proof: Proof. by elim: s1 => //= x s1 IHs; case: (a x) => //; rewrite IHs (fun_if succn). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)