proposition: Lemma Nat_sup_pr T (s:= \csup T) k: natp k -> (forall i, inc i T -> i <=c k) -> [/\ natp s, s <=c k, (forall i, inc i T -> i <=c s) & (T = emptyset \/ inc s T)].
proof: Proof. move=> kN km. case: (emptyset_dichot T) => Tne. rewrite /s Tne setU_0; split; fprops. by apply: cle0n. by move => i /in_set0. have pa: sub T (csucc k) by move => t /km /(NleP kN). have TN: sub T Nat by move => t /km h; apply:(NS_le_nat h kN). have fsT: finite_set T. apply:(sub_finite_set pa); apply: finite_set_nat; fprops. move: (@finite_subset_Nat T TN fsT Tne) => [n nT nm]. have pb: cardinal_set T by move => t /TN/CS_nat. have nN := TN _ nT. move: (cleA (card_ub_sup (CS_nat nN) nm) (card_sup_ub pb nT)) => eq. rewrite /s eq; split => //; [ by apply: km | by right ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)