proposition: Lemma Zermelo_chain_minimal1 r (E := substrate r): Zermelo_like r -> forall F, Zermelo_chain E F -> sub (segment_rs r) F.
proof: Proof. move => [wor ha] F zl => t /(segment_rs_P). have eF := (Zermelo_chain_least zl). case; first by move => ->. have or := proj1 wor. move: (zl) => [pa pb pc pd] [k kE ->]. move: k kE. apply:(transfinite_principle_bis wor) => x xsr H. case: (segment_r_succ_or_limit wor xsr). - by move ->. - move => [z /segmentP ltx ->]; move: (pc _ (H _ ltx)); rewrite ha //. order_tac. - move ->; case: (emptyset_dichot (segment r x)) => te. by rewrite te funI_set0 setI_0. apply:pd; last by apply: funI_setne. by move => u /funI_P [z /segmentP /H h ->]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)