proposition: Lemma first_non_int_p1 p n (i := first_non_int p n): natp n -> (i = n \/ (i <c n /\ ~ natp (p i))) /\ forall j, j <c i -> natp (p j).
proof: Proof. move => nN; rewrite /i/first_non_int. set E := Zo _ _. have snN := (NS_succ nN). have nsE: cardinal_set E by move => z /Zo_S /(NltP snN)/proj31_1. have nee: nonempty E. exists n; apply:Zo_i; [ by move/(NltP snN): (cltS nN) | by left]. move:(cle_wor' nsE nee) => [ /Zo_P [ /(NltP snN)ra rb] rc]; split. move/(cltSleP nN): ra => /cle_eqVlt; case; first by left. by move => lin; right; split => //; case:rb => // iE;case: (proj2 lin). move => j lji; ex_middle bad. case: (cltNge lji); apply: rc. apply:Zo_i; [ by apply/(NltP snN); apply: (clt_ltT lji ra) | by right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)