An extension of the SSReflect library with functions about sequences

The SSReflect library for sequences (https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html) 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.

Related