proposition: Lemma Exercise1_20b r: worder r -> scattered r.
proof: Proof. move=> wor;split; first by move: (wor) => [or _]. move=> z zsr. have : (worder (induced_order r z)) by apply: induced_wor. set (y:= induced_order r z). move=> woy [_ [a [b ab] yy]]. have asr: (inc a (substrate y)) by order_tac. set F := Zo (substrate y) (glt y a). have zs: (sub F (substrate y)) by apply: Zo_S. have bF: (inc b F) by apply/Zo_P; split => //; order_tac. have neF: (nonempty F) by exists b. move: woy => [oy woy]. move: (woy _ zs neF) => [d []]; rewrite iorder_sr // => /Zo_P [dd dle] dp. move: (yy _ _ dle)=> [e [e1 ne1] e2]. have eF: inc e F by apply/Zo_P; split => //; order_tac. move: (iorder_gle1 (dp _ eF)) => h; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)