proposition: Lemma Exercise2_3a r: order r -> exists A B, ex23_prop r A B.
proof: Proof. move=> or. pose no_least B := ~ has_least (induced_order r B). set (B:= union (Zo (\Po (substrate r)) no_least)). have Bsr: (sub B (substrate r)). by move=> t /setU_P [y ty] /Zo_S /setP_P; apply. move: (complement_p3 Bsr); set A := complement _ _. move=> [p1 p2]. exists A, B; split => //. have AE: (sub A (substrate r)) by apply: sub_setC. move: (iorder_osr or AE) => [or1 sr1]. split => //; rewrite sr1. move=> x xA [y yx]; rewrite iorder_trans //; ex_middle h. have xB: (sub x B). move=> t tx; apply: (setU_i tx); apply: Zo_i h. apply /setP_P; apply: (sub_trans xA AE). empty_tac1 y. move=> [y []];rewrite iorder_sr//. move => /setU_P [t yt aux] h; move: (aux) => /Zo_P [] /setP_P tr; case. exists y; split; rewrite iorder_sr// => x xt; apply /iorder_gle0P => //. exact: (iorder_gle1 (h _ (setU_i xt aux))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)