proposition: Lemma starts_with_aP l a: reflect (exists s, l = a::s) (l==a :: behead l).
proof: Proof. apply:(iffP idP). by move/eqP => ->; exists (behead l). by move => [s ->]. 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)