proposition: Lemma Nat_greatest A: sub A Nat -> nonempty A -> (exists x, upper_bound Nat_order A x) -> (has_greatest (induced_order Nat_order A)).
proof: Proof. move=> AB neA [w [_ wp]]. move:Nat_order_wor => [wor sr];move:(proj1 wor) => or. have asr: sub A (substrate Nat_order) by ue. apply: finite_set_torder_greatest; rewrite ? iorder_sr//. apply: (total_order_sub (worder_total wor) asr). apply: sub_finite_set (finite_Nintcc \0c w). by move => t /wp /Nat_order_leP [_ wN le]; apply/(NintcP wN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)