proposition: Lemma last_eq s z x y : x != y -> z != y -> (last x s == y) = (last z s == y).
proof: Proof. by move=> /negPf xz /negPf yz; case: s => [|t s]//; rewrite xz yz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)