proposition: Lemma last_ind P : P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s.
proof: Proof. move=> Hnil Hlast s; rewrite -(cat0s s). elim: s [::] Hnil => [|x s2 IHs] s1 Hs1; first by rewrite cats0. by rewrite -cat_rcons; apply/IHs/Hlast. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)