fact: Definition ends_with_ab l a b := l == rcons (rcons (rev (behead (behead (rev l)))) a) b.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)