proposition: Lemma Zermelo_like_chain_least1 r X: Zermelo_like r -> sub X (substrate r) -> nonempty X -> exists!Y, [/\ sub X Y, inc Y (segment_rs r) & inc (rep Y) X].
proof: Proof. move => [pa pb] XE neX. have or: order r by fprops. apply/unique_existence; split. move:(proj2 pa _ XE neX) => [y []]. rewrite (iorder_sr or XE)=> yX yP. have yE := (XE _ yX). have ha:sub X (segment_r r y). by move => t /yP /iorder_gle1 tX; apply /segment_rP. move/(segment_rs_p1 pa): (segment_r_p1 or yE) => hb. have hc:inc (rep (segment_r r y)) X by rewrite pb. by exists (segment_r r y). move => Y1 Y2 [qa qb qc] [qd qe qf]. have [x0 x0X] := neX. case/segment_rs_P: qb; last move => [y1 y1sr Y1v]. by move => ye; move:(qa _ x0X); rewrite ye => /in_set0. case /segment_rs_P:qe; last move => [y2 y2sr Y2v]. by move => ye; move:(qd _ x0X); rewrite ye => /in_set0. move: qc qf qa qd; rewrite Y1v Y2v pb // pb // => qc qf y1X y2X. move:(y2X _ qc); move/segment_rP => sa. move:(y1X _ qf); move/segment_rP => sb. f_equal; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)