proposition: Lemma set_head_default b a s : s != [::] -> head a s = head b 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)