proposition: Lemma chain_valP x i: inc i (chain_val x) <-> (exists2 p, sub_chain p x & i = chain_head p).
proof: Proof. split. elim:x => a x /=. by move /set1_P ->; exists (chain_pair a x). move => Hrec /setU1_P; case => aux. by move: (Hrec aux) => [p p1 p2]; exists p => //; right. by exists (chain_next a x) => //; left. move => [p]. elim: x => a x /=; first by move => -> -> /=; fprops. move => Hrec p1 p2; case: p1; first by rewrite p2; move => -> /=; fprops. by move => p3; apply /setU1_P; left; apply: Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)