proposition: Lemma chain_val_finite x: finite_set (chain_val x).
proof: Proof. elim: x => [pa pb /=| pa pb /= Hrec]; first by apply: set1_finite. by apply: setU1_finite. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)