proposition: Lemma Zermelo_omega_chain r (E := substrate r): Zermelo_like r -> Zermelo_chain E (segment_rs r).
proof: Proof. move => [ha hb]; move: (ha) => [or wor]. have ra: sub (segment_rs r) (\Po E). by move => t /(segment_rs_p1 ha) [/setP_P ts _]. have rb: inc (substrate r) (segment_rs r). apply/(segment_rs_p1 ha); split => // x y xsr le; order_tac. have rc: forall A, inc A (segment_rs r) -> inc (A -s1 rep A) (segment_rs r). move => A /segment_rs_P; case. by move => ->; apply /setU1_P; right;apply/set0_P => t /setC1_P [/in_set0]. move => [z zE ->]; rewrite (hb _ zE). by apply/(segment_rs_p1 ha) /segment_rp_p2. split => // A Aom neA; apply/(segment_rs_p1 ha). by apply:(segment_rp_p3 or) => t /Aom /(segment_rs_p1 ha). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)