proposition: Lemma cons_head_behead x s : (s != [::]) -> head x s :: behead s = s.
proof: Proof. Proof using. by case s. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)