proposition: Lemma Exercise2_8c r a: order r -> inc a (substrate r) -> exists A, maximal (sub_order (Exercise2_8a_R r a)) A.
proof: Proof. move=> or ar; apply: Zorn_lemma; first by fprops. red; aw; set (F := Exercise2_8a_R r a). move: (sub_osr F) => [oF sF]. move => X Xsr []; rewrite iorder_sr // => [oX toX]; rewrite /upper_bound sF. have asr: sub (singleton a) (substrate r) by move => t /set1_P ->. have leX: (forall x y, inc x X -> inc y X -> sub x y \/ sub y x). move => x y xX yX; move: (toX _ _ xX yX). case => aux; move: (iorder_gle1 aux) => /sub_gleP [_ _ h]; in_TP4. case: (emptyset_dichot X)=>xe. exists (singleton a); split. apply: Zo_i; first by apply /setP_P; apply: set1_sub. split. by move=> x y [cxy]; move: (iorder_gle3 cxy) => [] /set1_P -> /set1_P ->. red; rewrite iorder_sr//;split;fprops;move=> x /set1_P ->; apply /iorder_gle0P;fprops. by order_tac. move => y yX; empty_tac1 y. rewrite sF in Xsr. have uX: (inc (union X) F). rewrite /F (Exercise2_8b _ _ or); split => //. move=> t /setU_P [y ty yX]; move: (Xsr _ yX) => /Zo_P. by move=> [yp _]; move: yp => /setP_P; apply. move => x y xy /setU_P [x' xx' xX'] /setU_P [y' yy' yX']. have [z [zX xz yz]] : (exists z, [/\ inc z X, inc x z & inc y z]). case: (leX _ _ xX' yX') => xy';[ exists y'| exists x']; split; fprops. move: (Xsr _ zX); rewrite (Exercise2_8b _ _ or); move=> [_ h _]. move: (h _ _ xy xz yz) => [t [t1 t2 t3 t4]]; exists t; split => //. union_tac. move: xe => [e ex]; move: (Xsr _ ex); rewrite (Exercise2_8b _ _ or). move=> [_ _ h _]; union_tac. move=> z /setU_P [x zx zX]; move: (Xsr _ zX). by rewrite (Exercise2_8b _ _ or); move=> [_ _ _ ]; apply. exists (union X); split => //. by move => x xF;apply/sub_gleP;split;fprops; apply: setU_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)