proposition: Lemma belast_cat x s1 s2 : belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2.
proof: Proof. by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)