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