The SSReflect library for sequences (GitHub) does not include any functions to check whether a sequence is a subchain of another one, i.e., a consecutive subsequence.

Our team developed this function, together with suffix and prefix, and all the required theorems about them to contribute to the MathComp SSReflect library.

See (GitHub)
An important issue for the use of Coq in industrial developments is its treatment of natural numbers and integers. As a mathematical programming language, Coq defines these numbers in a way that is useful to prove theorems about them, but is too inefficient to use in practical executions. To solve this problem, recently Coq introduced the Int63 type, which gives efficient machine unsigned integers available inside Coq. However, signed integers continued being unavailable, so the \textit{Prometheuss - Proof Methods for European Software Systems} team contributed them to Coq. They are called Sint63 and are now part of the latest Coq development branch, and will be part of the next official release of a Coq version.

After facing the frequent practical problem of bounding an arithmetical expression (for instance, to prove that overflow will not occur) and experiencing the intrinsic difficulties of proving such inequalities using mathematical arguments inside Coq, the team was able to develop a tool for automating this kind of task. In particular, the tool instructs Coq to the extent that it can compute all the cases and check that the inequality holds for each of them, and thus deduce that the inequality holds in general. This tool is developed for inequalities on types Int63 and Sint63, and is planned to be released for other Coq types.