proposition: Lemma chained_prop1 g a c: chained_r (fun a b => a = g b) c -> chain_tail c = a -> sub_chain (chain_pair (g a) a) c.
proof: Proof. elim:c => b x /=; first by move => -> ->. by move => Hrec [p1 p2] p3; right; apply: Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)