proposition: Lemma ends_with_aP l a : reflect (exists w, l = (rcons w a)) (ends_with_a l a).
proof: Proof. apply: (iffP idP). by move/eqP ->; set x:=(belast _ _); exists x. by move=> [w ->]; rewrite ends_with_aE /ends_with_a' 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)