proposition: Lemma ends_with_ab_cons x l a b: ends_with_ab l a b -> ends_with_ab (x::l) a b.
proof: Proof. move/ ends_with_abP => [w ->]. by rewrite/ends_with_ab rev_cons !rev_rcons revK. Qed.
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)