proposition: Lemma subseq_trans : transitive subseq.
proof: Proof. move=> _ _ s /subseqP[m2 _ ->] /subseqP[m1 _ ->]. elim: s => [|x s IHs] in m2 m1 *; first by rewrite !mask0. case: m1 => [|[] m1]; first by rewrite mask0. case: m2 => [|[] m2] //; first by rewrite /= eqxx IHs. case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP. by exists (false :: m); rewrite //= sz_m. case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP. by exists (false :: m); rewrite //= sz_m. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)