proposition: Lemma pairmap_cat x s1 s2 : pairmap x (s1 ++ s2) = pairmap x s1 ++ pairmap (last x s1) s2.
proof: Proof. by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)