proposition: Lemma chain_equivalence_eq: equivalence_on chain_equivalence E.
proof: Proof. split; last by apply: graph_on_sr => x /chain_related_re. apply: equivalence_from_rel. split. move=> x y [c [cc hcx tcy]]. exists (chain_reverse c); split. + by apply: chained_reverse. + by rewrite head_reverse. + by rewrite tail_reverse. move => y x z [c [cc hcx tcy]][c' [cc' hcy tcz]]. exists (concat_chain c c'); split => //. apply: chained_concat=>//; ue. by rewrite head_concat. by rewrite tail_concat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)