proposition: Lemma Zermelo_chain_minimal r (E := substrate r): Zermelo_like r -> (segment_rs r) = intersection (Zo (\Po (\Po E)) (Zermelo_chain E)).
proof: Proof. move => h. set Z := Zo _ _. have w: forall F, inc F Z <-> Zermelo_chain E F. move => f; split;first by move/Zo_hi. by move => zc; apply: Zo_i => //; apply /setP_P; move: zc=> []. have ha: inc (segment_rs r) Z by apply/w/Zermelo_omega_chain. set_extens t; last by move => ts; exact:(setI_hi ts ha). move => ts; apply/setI_P; [ex_tac | move => i /w ci]. exact: (Zermelo_chain_minimal1 h ci ts). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)