proposition: Lemma least_int_prop2 n (p: property) (x:= cpred (least_ordinal p n)): natp n -> p n -> p \0c \/ [/\ natp x, p (csucc x) & ~ p x].
proof: Proof. move => ha hb. move: (least_int_prop ha hb) => [qa qb qc]. case: (equal_or_not (least_ordinal p n) \0c); first by move <-;left. move => zp; right; move: (cpred_pr qa zp) => [qd qe]; rewrite - qe. split => //. by move => px; case:(cleNgt(qc _ qd px)); rewrite {2} qe; apply: cltS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)