proposition: Lemma finite_subset_Nat X: sub X Nat -> finite_set X -> nonempty X -> exists2 n, inc n X & forall m, inc m X -> m <=c n.
proof: Proof. move => pa pb pc. move: (wordering_cle_pr CS_nat) => [wor sr]. have pd: sub X (substrate (graph_on cardinal_le Nat)) by rewrite sr. move: (finite_subset_torder_greatest (worder_total wor) pb pc pd). move => [n []]; rewrite (iorder_sr (proj1 wor) pd) => pe pf; ex_tac. by move => m /pf /iorder_gle1/graph_on_P0/proj33. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)