proposition: Lemma Exercise5_9l6bis q n k J j x : Ex59_Jprop q n k J -> natp k -> \0c <c k -> natp x -> j <c k -> j <> \0c -> (nth_elt J (cpred j)) <c x -> x <=c (nth_elt J j) -> Ex59_pos_in_J J k x = j.
proof: Proof. move => H kN kp xN ljk jna ha hb. move:(Exercise5_9l6 H kN kp) => [ra rb rc rd re]. move: (Exercise5_9k2 kN H) => [jp1 jp2 jp3 jp4 jp5]. have K u v: u <c v -> v <c k -> nth_elt J (cpred v) <c nth_elt J u -> False. move => luv lvk lt1. move: (cpred_pr (NS_lt_nat lvk kN) (card_gt_ne0 luv)) => [ua ub]. have la: u <=c cpred v by apply /(cltSleP ua); rewrite - ub. case:(cleNgt (jp2 _ _ la (cle_ltT (cpred_le (proj31_1 lvk)) lvk)) lt1). move: (cpred_pr (NS_lt_nat ljk kN) jna) => [ua ub]. have jJ: inc (nth_elt J j) J by apply: jp4. have pjs: cpred j <c j by rewrite {2} ub; fprops. have cpjk:=(clt_ltT pjs ljk). move: (ra x); set v := Ex59_pos_in_J J k x; case /cle_eqVlt => vk. by move /(rc _ xN): vk => h; move:(cltNge (h _ jJ) hb). case: (equal_or_not v \0c) => vz. by move/rb:vz => h; move:(cleNgt (h _ (jp4 _ cpjk)) ha). have vz':=(card_ne0_pos (proj31_1 vk) vz). move: (re _ vz' vk); rewrite -/v; move => [la lb lc ld]. move: (clt_leT ha lb) (clt_leT ld hb) => le lf. case:(cleT_ell (proj31_1 vk) (proj32_1 pjs)) => // h. - case: (K _ _ h ljk le). - case: (K _ _ h vk lf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)