proposition: Lemma belast_behead_rcons x l s : belast (head x (rcons s l)) (behead (rcons s l)) = s.
proof: Proof. Proof using. by case: s => // s0 s; rewrite rcons_cons belast_rcons. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)