proposition: Lemma chained_reconc x y: chained_r x -> chained_r y -> R (chain_head y) (chain_head x) -> chained_r (reconc_chain x y).
proof: Proof. move: x y; elim => [a b y c cy | P c r]=>//=; auto. by move=> y [rPh cc] cy RhyP; apply: r=>//; split => //; apply: A2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)