proposition: Lemma prefix_drop_sub (s1 s2 : seq A) : seq.prefix s1 s2 -> forall n, {subset (drop n s1) <= drop n s2}.
proof: Proof. case/seq.prefixP=>s0 {s2}-> n x H. rewrite drop_cat; case: ltnP=>Hn. - by rewrite mem_cat H. by move: H; rewrite drop_oversize. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)