proposition: Lemma chained_reverse x: chained_r x -> chained_r (chain_reverse x).
proof: Proof. elim: x; first by move=> a b;apply:A2. move=> a; elim; first by move => b c /= _ [/A2 h2 /A2 h3]. move=> b c hr hr1 /= [/A2 Rab [Rbc cc]]. by apply: chained_reconc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)