proposition: Lemma ns_extensions_prop2 z: inc z ns_extensions <-> [/\ sub ns_compare z, order_on z C & total_order z].
proof: Proof. split. move =>/ns_extensions_prop1 [ha [hb hc]];split => //; first by case:hb. by apply: worder_total. move => [ha [hb hc] hd]; apply/ns_extensions_prop1; split => //; split => //. apply: (worder_prop_rev hb); rewrite hc => X XC neX. set X0 := Zo X (fun z => Q z = C0). set X1 := Zo X (fun z => Q z = C1). have nes: nonempty X0 \/ nonempty X1. case: neX => t tX; case/candu2P: (XC t tX) => pt; case => -[qa qb]. by left; exists t; apply: Zo_i. by right; exists t; apply: Zo_i. move: (wor1) (wor2) => [wo1 sr1] [wo2 sr2]. have Ha: nonempty X0 -> exists2 a, inc a X0 & forall b, inc b X0 -> gle z a b. move => nex0; pose Y := fun_image X0 P. have neY: nonempty Y by apply: funI_setne. have sY:sub Y (substrate rA). rewrite sr1; move => t /funI_P [u /Zo_P[uX qu] ->]. move /candu2P:(XC _ uX) => [_]; case; case => //; rewrite qu => _ bb. by case:C1_ne_C0. move:(worder_prop wo1 sY neY) =>[a aY av]. move/funI_P:aY => [b bX bp]; ex_tac. move/Zo_P: bX => [bX Qb]. move => c /Zo_P [qa qb]; apply: ha; apply/graph_on_P1; split. by apply: XC. by apply: XC. left; split => //; rewrite - bp; apply:av; apply/funI_P; exists c => //. by apply: Zo_i. have Hb: nonempty X1 -> exists2 a, inc a X1 & forall b, inc b X1 -> gle z a b. move => nex0; pose Y := fun_image X1 P. have neY: nonempty Y by apply: funI_setne. have sY:sub Y (substrate rB). rewrite sr2; move => t /funI_P [u /Zo_P[uX qu] ->]. move /candu2P:(XC _ uX) => [_]; case; case => //; rewrite qu => _ bb. by case:C1_ne_C0. move:(worder_prop wo2 sY neY) =>[a aY av]. move/funI_P:aY => [b bX bp]; ex_tac. move/Zo_P: bX => [bX Qb]. move => c /Zo_P [qa qb]; apply: ha; apply/graph_on_P1; split. by apply: XC. by apply: XC. have qbz: Q b <> C0 by rewrite Qb; fprops. have qcz: Q c <> C0 by rewrite qb; fprops. right; split => //; rewrite - bp; apply:av; apply/funI_P; exists c => //. by apply: Zo_i. case: (emptyset_dichot X0) => x0e. have eq1: X = X1. set_extens t; [ move => tx; apply:Zo_i => // | by move/Zo_S ]. move/candu2P:(XC _ tx) =>[_]; case; case => _ qa //. by empty_tac1 t; apply: Zo_i. rewrite eq1; apply: Hb; ue. case: (emptyset_dichot X1) => x1e. have eq1: X = X0. set_extens t; [ move => tx; apply:Zo_i => // | by move/Zo_S ]. move/candu2P:(XC _ tx) =>[_]; case; case => _ qa //. by empty_tac1 t; apply: Zo_i. rewrite eq1; apply: Ha; ue. move: (Ha x0e) (Hb x1e) =>[a ax0 ap][b bx0 bp]. have ap1 x: inc x X -> Q x = C0 -> gle z a x. by move => sa sb; apply: ap; apply:Zo_i. have bp1 x: inc x X -> Q x <> C0 -> gle z b x. move => sa sb; apply: bp; apply:Zo_i => //. move/candu2P:(XC _ sa) =>[_];case;case => //. move: (Zo_S ax0) (Zo_S bx0) => aX bX. have asz: inc a (substrate z) by rewrite hc; apply: XC. have bsz: inc b (substrate z) by rewrite hc; apply: XC. case: (proj2 hd a b asz bsz) => le. exists a => //x xX; case: (equal_or_not (Q x) C0) => qx. by apply: ap1. by move:(bp1 x xX qx) => ll; order_tac. exists b => //x xX; case: (equal_or_not (Q x) C0) => qx. by move:(ap1 x xX qx) => ll; order_tac. by apply: bp1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)