proposition: Lemma pairmap_bseqP f x s : @size rT (pairmap f x s) <= n.
proof: Proof. by rewrite size_pairmap size_bseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)