proposition: Lemma BZ_N_worder X: sub X BZp -> nonempty X -> exists2 a, inc a X & forall b, inc b X -> BZ_le a b.
proof: Proof. move => pa [t tx];set (Y:= fun_image X P). have yb: sub Y Nat. move => y /funI_P [z zz ->]; apply: (BZ_valN (BZp_sBZ (pa _ zz))). have ney: (nonempty Y) by exists (P t); apply /funI_P; ex_tac. move: (Nat_order_wor) => [[or wor] sr]. have yb1: sub Y (substrate Nat_order) by rewrite sr. move: (wor _ yb1 ney) => [y []]; rewrite iorder_sr // => yy aux. move /funI_P: (yy) => [z zx pz]; ex_tac. move => b bx; apply /(zle_P1 (pa _ zx) (pa _ bx)); rewrite - pz. have pby: inc (P b) Y by apply /funI_P; ex_tac. by move: (iorder_gle1 (aux _ pby)) => /Nat_order_leP [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)