proposition: Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2.
proof: Proof. wlog suff W : s1 s2 / subseq s1 s2 -> subseq (rev s1) (rev s2). by apply/idP/idP => /W //; rewrite !revK. by case/subseqP => m size_m ->; rewrite rev_mask // mask_subseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)