proposition: Lemma finite_subset_ord X: finite_set X -> nonempty X -> ordinal_set X -> exists2 n, inc n X & forall m, inc m X -> m <=o n.
proof: Proof. move: X; apply: finite_set_induction2. move => a oa; exists a; fprops => b bb; move: (oa _ bb) => /oleR. by rewrite (set1_eq bb). move => a b Hrec nea osab. have osa: ordinal_set a. move => t ta; apply: osab; fprops. move:(Hrec nea osa) =>[c ca cg]. have osb: ordinalp b by apply:osab; fprops. have osc: ordinalp c by apply: osa. move: (omax_p1 osb osc)=> [qa qb]. exists (omax b c); first by rewrite/omax/Gmax; Ytac w; fprops. move => t /setU1_P; case; first by move/cg => tt; apply:(oleT tt qb). by move ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)