proposition: Lemma Exercise2_6g r a (m := Zo (substrate r) (fun z => glt r a z)) : worder r -> inc a (substrate r) -> nonempty m -> exists2 b, inc b (substrate r) & (segmentc r a = segment r b).
proof: Proof. move=> wor asr nem. move: (worder_total wor) => tor. have sms: (sub m (substrate r)) by apply: Zo_S. move: wor => [or wor1]; move: (wor1 _ sms nem) => [y[]]; rewrite iorder_sr // => ym yl. move: (sms _ ym) => ysr; ex_tac. move: (ym)=> /Zo_hi ya. set_extens t; first by move /segmentcP => ta; apply /segmentP; order_tac. move /segmentP => ta; apply /segmentcP. have tsr: inc t (substrate r) by order_tac. case: (total_order_pr2 tor asr tsr) => // lat. have tm: inc t m by apply: Zo_i. move: (iorder_gle1 (yl _ tm)) => h'; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)