proposition: Lemma Exercise1_20c r: scattered r -> Exercise1_20_prop r.
proof: Proof. move=> [or sc] x y xy. set (F:= interval_cc r x y). have Fs: (sub F (substrate r)) by apply: Zo_S. move: (iorder_osr or Fs)=> [or1 sr1]. move: (sc _ Fs) => nw; ex_middle bad; case: nw;split => //. have xsr: inc x (substrate r) by order_tac. have ysr: inc y (substrate r) by order_tac. exists x, y; move: xy => [xy nxy]; split; last by exact. by apply /iorder_gle0P => //; apply: Zo_i =>//; split => //; order_tac. move => a b ab. have ab2: (glt r a b) by apply: (iorder_gle2 ab). move: (iorder_gle4 ab) => [aF bF]. move: (iorder_gle4 ab) => [] /Zo_hi [xa _] /Zo_hi [_ lby]. ex_middle bad1; case: bad;exists a,b;split => // z [[az anz] [bz bnz0]]. have zF: inc z F by apply: Zo_i; [ order_tac | split => //; order_tac]. by case: bad1; exists z; split => //;apply /iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)