proposition: Lemma Zermelo_unique r r': Zermelo_like r -> Zermelo_like r' -> substrate r = substrate r' -> r = r'.
proof: Proof. move => ha hb ss. have ch12: (segment_rs r) = (segment_rs r'). rewrite (Zermelo_chain_minimal ha). by rewrite (Zermelo_chain_minimal hb) ss. move: ha hb => [wor1 ha] [wor2 hb]. move:(wor1)(wor2) => [or1 _][or2 _]. have pa: forall x, inc x (substrate r) -> segment_r r x = segment_r r' x. move => x xsr. have: inc (segment_r r x) (segment_rs r'). by rewrite - ch12; apply/setU1_P; left; apply/funI_P; ex_tac. case /setU1_P. move/funI_P => [z za ea]; rewrite ea. by move:(f_equal rep ea); rewrite (ha _ xsr) (hb _ za) => ->. by move => h; empty_tac1 x; apply/segment_rP; order_tac. apply:order_exten => // x y. case: (inc_or_not x (substrate r)) => xE; last first. split => h; case xE; [ | rewrite ss ]; order_tac. have ssx:=(pa _ xE). split => /segment_rP; first by rewrite ssx => /segment_rP. by rewrite - ssx => /segment_rP. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)