proposition: Lemma chained_concat x y: chained_r x -> chained_r y -> chain_tail x = chain_head y -> chained_r (concat_chain x y).
proof: Proof. move=> cx cy txhy;elim: x cx txhy => [a b cp ct| a c r cp ct]. split=>//; by rewrite -ct //. by move: cp => [pa pb];split; [rewrite head_concat | apply: r]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)