proposition: Lemma ends_with_aE a l: (ends_with_a l a) = (ends_with_a' l a).
proof: Proof. by rewrite /ends_with_a /ends_with_a'; case:l => // b l; rewrite rev_behead_etc. 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)