proposition: Lemma set_compare_to_finite E n: natp n -> E <s n \/ n <=s E.
proof: Proof. move: n; apply: Nat_induction. by right; apply: set_le_t => t /in_set0. move => n nN. move: (succ_of_nat nN) => r1. have ha: n <=s csucc n. by apply:set_le_t; rewrite r1 => t tx; apply: setU1_r. case; first by move => hb;move:(set_lt_leT hb ha) => hc; left. move => /set_leP [X sXE exn]. move/NatP: (nN)=> [/ordinal_irreflexive nn fn]. case: (equal_or_not X E) => xe. rewrite - xe; left; split; first by move: (set_le_i1 ha exn). rewrite r1; move => h;case fn; exact:(EqT exn h). move: (setC_ne (conj sXE xe)) => [y /setC_P[yE ynX] ]; right. apply /set_leP; exists (X +s1 y); first by apply: setU1_sub. by rewrite r1; apply/(succ_inf_aux_p1). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)