proposition: Lemma sub_chainedP R p q: sub_chain p q -> chained_r R q -> chained_r R p /\ chain_tail p = chain_tail q.
proof: Proof. move => p1 p2; split. move: p1 p2; elim q => a x /=; first by move => -> /=. move => Hrec; case => aux; first by rewrite aux /= => []. by move => [p1 p2]; apply: Hrec. clear p2; move: p1; elim: q => a x /=; first by move => -> /=. move => Hrec; case => aux; [ by rewrite aux | by apply: Hrec]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)