proposition: Lemma Exercise5_9l6 q n k J: Ex59_Jprop q n k J -> natp k -> \0c <c k -> [/\ forall x, Ex59_pos_in_J J k x <=c k, forall x, Ex59_pos_in_J J k x = \0c <-> (forall y, inc y J -> x <=c y), forall x, natp x -> (Ex59_pos_in_J J k x = k <-> (forall y, inc y J -> y <c x)), forall x, (exists2 y, inc y J & x <=c y) -> (exists2 y, inc y J & y <c x) -> (\0c <c Ex59_pos_in_J J k x /\ Ex59_pos_in_J J k x <c k) & forall x, let i := Ex59_pos_in_J J k x in \0c <c i -> i <c k -> [/\ inc (nth_elt J i) J, x <=c (nth_elt J i), inc (nth_elt J (cpred i)) J & (nth_elt J (cpred i)) <c x ]].
proof: Proof. move => Jp kN kp. pose Ex x := (Zo (Nint k) (fun i=> x <=c nth_elt J i) +s1 k). pose lEx x := intersection (Ex x). have ha: forall x, sub (Ex x) (Nintc k). move => x t /setU1_P; case. by move =>/Zo_S /(NintP kN) [ /(NintcP kN)]. move => ->; apply/(NintcP kN); fprops. have hb x: inc (lEx x) (Ex x) /\ forall y, inc y (Ex x) -> (lEx x) <=c y. have px: sub (Ex x) Nat by move => t/ha /Nint_S. have pa: ordinal_set (Ex x) by move => t /px/OS_nat. have pb: nonempty (Ex x) by exists k; apply: setU1_1. move:(least_ordinal0 pa pb); rewrite -/(lEx x); move => [sa sb sc]. split => // y ya. exact: (ocle3 (CS_nat (px _ sb)) (CS_nat (px _ ya)) (sc _ ya)). have hc x: (lEx x) <=c k. apply/(NintcP kN); exact (ha _ _ (proj1 (hb x))). move: (Exercise5_9k2 kN Jp) => [jp1 jp2 jp3 jp4 jp5]. have ra x: lEx x = \0c -> (forall y, inc y J -> x <=c y). move => pp; move: (proj1 (hb x)); rewrite pp; case/setU1_P; last first. by move => kz; case: (proj2 kp). move/Zo_hi =>xs y /jp5 [j ljk ->]. exact:(cleT xs (jp2 _ _ (cle0x (proj31_1 ljk)) ljk)). have rb: forall x, (forall y, inc y J -> x <=c y) -> lEx x = \0c. move => x hx. have /(proj2(hb x))/cle0//: inc \0c (Ex x). apply:setU1_r; apply:Zo_i; first by apply/(NintP kN). exact:(hx _ (jp4 _ kp)). move:Jp =>[wa JN _ _]. have rc: forall x, natp x -> lEx x = k -> (forall y, inc y J -> y <c x). move => x xN lk; move: (hb x) => [_]; rewrite lk => xb. move => y /jp5 [i ik ->]; case:(NleT_el xN (JN _ (jp4 _ ik))) => // xc. have: inc i (Ex x) by apply setU1_r; apply:Zo_i => //; apply/(NintP kN). by move /xb => /(cltNge ik). have rd: forall x, (forall y, inc y J -> y <c x) -> lEx x = k. move => x hx; move: (hb x) => [xa xb]. by case /setU1_P:xa => // /Zo_P [/(NintP kN) /jp4/hx sa /cleNgt []]. have re: forall x, (exists2 y, inc y J & x <=c y) -> (exists2 y, inc y J & y <c x) -> (\0c <c lEx x /\ lEx x <c k). move => x [y1 y1j la] [y2 y2j lb]. have nN:=(NS_le_nat la (JN _ y1j)). have hcx := hc x. split. by apply:(card_ne0_pos (proj31 hcx)) => /ra ee; case:(cleNgt (ee _ y2j)). by split => // /(rc _ nN) ee;case: (cltNge (ee _ y1j)). split => //. - move => x; split;fprops. - move => x; split;fprops. - move => x i xa xb; move:(hb x) => [/setU1_P xc xd]. case: xc; [ move/Zo_hi => xe | by move => h; case: (proj2 xb) ]. have sa:= (jp4 _ xb). have sc:= (cpred_lt (NS_lt_nat xb kN) (nesym (proj2 xa))). have sb' := (clt_ltT sc xb). have sb:= (jp4 _ sb'). split => //; case: (NleT_el (NS_le_nat xe (JN _ sa))(JN _ sb)) => // xh. have /xd /cleNgt sd //: inc (cpred (lEx x)) (Ex x). by apply:setU1_r; apply: Zo_i => //; apply/(NintP kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)