proposition: Lemma chain_equivalence_is_smallest: chain_equivalence = eqv_smallest E R.
proof: Proof. apply:eqv_smallest_prop2. + move => x y rxy;split; [exact: (A3 rxy)| exact (A3 (A2 rxy))]. + exact chain_equivalence_eq. + move => x y Rxy;apply/graph_on_P1; split. - apply: (A3 Rxy). - apply: (A3 (A2 Rxy)). - exists (chain_pair x y); split => //. + move => r' [er' _] p q. have aux:(forall w, chained_r w -> inc (J (chain_head w) (chain_tail w)) r'). elim => [a b | a c h [aux cc]] //=; first by apply: p. move: (h cc)(p _ _ aux) => r1 r2; apply:(proj43 er' _ _ _ r2 r1). move /Zo_P => [pp [c [cc hcx htx]]]. have <-: (J (P q)(Q q) = q) by move/setX_P: pp => [pp _]. by rewrite -hcx -htx ; apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)