proposition: Lemma finite_subset_Nat_bis A: sub A Nat -> finite_set A -> exists2 m, natp m & forall n, inc n A -> n <c m.
proof: Proof. move => sN fs. case: (emptyset_dichot A) => se. by rewrite se; exists \0c; [ fprops | move => m /in_set0]. move: (finite_subset_Nat sN fs se) =>[n /sN nN nb]; exists (csucc n). by apply: NS_succ. by move => m /nb /(cltSleP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)