proposition: Lemma nn_to_n_check_end l: exists w k, l = w ++ nseq k false /\ (w== nil) || ends_with_a w true.
proof: Proof. elim: l; first by exists nil,0. move => a l [w [k [-> /orP []]]]. move/eqP ->; case:a; [ by exists [:: true], k | by exists nil, k.+1 ]. by move => /(ends_with_a_cons a); exists (a::w),k. 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)