fact: Fixpoint reconc_chain (x y:chain) :chain:= match x with chain_pair u v => chain_next v (chain_next u y) | chain_next u v => reconc_chain v (chain_next u y) end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)