proposition: Lemma chained_prop2 g p c: chained_r (fun a b => a = g b) c -> sub_chain p c -> p = c \/ sub_chain (chain_next (g (chain_head p)) p) c.
proof: Proof. elim:c => a c /=; first by left. move => Hrec [p1 p2]; case => p3; first by left. case: (Hrec p2 p3); last by right; right. by move => epc; right; left; rewrite epc -p1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)