proposition: Lemma DP_splitb_lastT l: ends_withT (DP_splitb (rcons l true)).2.
proof: Proof. elim:l => // a l H /=. case: (nilp (DP_splitb (rcons l true)).1) => //. have hb: last a (DP_splitb (rcons l true)).2 == true. by move: H; case: (DP_splitb (rcons l true)).2. by case nl: (nilp _); [ move: H;move/nilP:nl => -> | case: ifP ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)