proposition: Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
proof: Proof. set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat drop_cat. rewrite size_rev size_drop -minnE minnC leq_min ltnn /m. by have [_|/eqnP->] := ltnP; rewrite ?take0 // subnn drop0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)