proposition: Lemma Exercise5_9l7 q n k J (e := nth_elt J) (E' := (Ex59_compl n q J)): natp n -> natp q -> \0c <c q -> k <=c n -> Ex59_Jprop q n k J -> natp k -> \0c <c k -> (inc (cpred (q *c n)) E' \/ ( (forall t, inc t E' -> t <c q *c (n -c k)) \/ exists j, let x := (q *c ((n -c k) +c j)) in [/\ j <c k, x <> \0c, e j = x, inc (cpred x) E' & forall t, inc t E' -> t <=c (cpred x)])).
proof: Proof. move => nN qN qp lkn jP kN kp. move: (Exercise5_9k2 kN jP) => [jp1 jp2 jp3 jp4 jp5]. move: (jP) =>[cJ JN jp6 jp7]. pose di i := q *c (n -c i -c \1c). have qnN:= NS_prod qN nN. have knz :=(nesym (proj2 kp)). have q0:=(nesym (proj2 qp)). have np := (clt_leT kp lkn). have nnz := (nesym (proj2 np)). have [pnN pnv ]:=(cpred_pr nN nnz). have cpq:= (cpred_pr4 (CS_nat qN)). have cpk:= (cpred_pr4 (CS_nat kN)). have lpkk:= (cpred_lt kN knz). have [pkN pkv]:= (cpred_pr kN knz). have qnz:=(cprod2_nz q0 nnz). have [yN yv]:=(cpred_pr qnN qnz). have yE1:=(cpred_lt qnN qnz). set y0 := cpred (q *c n) in yN yv yE1. case: (inc_or_not y0 E') => yE; [by left | right]. have E'b t: inc t E' -> t <c q *c n by move => /setC_P [/(NintP qnN)]. have EN : sub E' Nat by move => t /E'b h;exact: (NS_lt_nat h qnN). have div i: i <c n -> di i = q *c (n -c (csucc i)). move => licn; move:(NS_lt_nat licn nN) => iN. move:(Nsucc_rw iN) => sa; rewrite sa. rewrite /di;apply: f_equal; rewrite (cdiffA nN iN NS1) //; rewrite - sa. by apply/(cleSltP iN). have div1 i: i <c n -> di i +c q *c (csucc i) = q *c n. move => licn; move:(NS_lt_nat licn nN) => iN. by rewrite (div _ licn) - cprodDr csumC (cdiff_pr) //; apply/(cleSltP iN). have ddN i : natp (n -c i -c \1c) by apply:NS_diff; apply:NS_diff. have diN i: natp (di i) by apply: (NS_prod qN (ddN i)). pose II j := (Nintcc j (j +c (q -c \1c))). have IIP j: natp j -> forall x, inc x (II j) <-> j <=c x /\ x <c j +c q. move => jN x; apply:(Ex59_interval_prop jN qN qp). have [j0 j0j yJ]: exists2 j, inc j J & inc y0 (II j). case: (inc_or_not y0 (union (fun_image J II))) => yz. by move/setU_P: yz => [v va /funI_P [j ja jb]]; ex_tac; rewrite - jb. by case: yE; apply/setC_P; split => //; apply/(NintP qnN). have j1p:j0 +c q = q *c n. apply: cleA; first by move: (jP) => [_ _ _ sa]; exact:(sa _ j0j). move/(IIP _ (JN _ j0j)): yJ =>[_]. by rewrite yv; move/(cleSlt0P (proj31_1 yE1) (NS_sum (JN _ j0j) qN)). have j0v: j0 = di \0c. rewrite /di (cdiff_n0 nN)(cprodBl qN nN NS1) - j1p (cprod1r (CS_nat qN)). by rewrite (cdiff_pr1 (JN _ j0j) qN). have j0max: forall j, inc j J -> j <=c j0. move => j r1;move: (jp7 _ r1); rewrite -j1p => r2. exact:(csum_le2r qN (JN _ r1) (JN _ j0j) r2). have la0: e (k -c \1c) = di \0c. rewrite - cpk - j0v; apply:cleA; first exact:(j0max _ (jp4 _ lpkk)). move:(jp5 _ j0j) => [a a1 ->]. move: a1; rewrite {1} pkv; move /(cltSleP pkN) => a1. by move: (jp2 a (cpred k) a1 lpkk). have div0 i p: natp i -> natp p -> csucc i <c p -> csucc ((p -c csucc i) -c \1c) = ((p -c i) -c \1c). move => iN pN sa. have ea:= Nsucc_rw iN. have la: i +c \1c <=c p by move: (proj1 sa); rewrite ea. rewrite (cdiffA pN iN NS1 la) - ea -(cpred_pr4 (CS_diff _ _)). by rewrite -(proj2 (cpred_pr (NS_diff (csucc i) pN) (cdiff_nz sa))). have div2 i: natp i -> csucc i <c n -> di (csucc i) +c q = di i. move => iN sa;rewrite -(cprod_nS _ (ddN _)) /di. rewrite (div0 _ _ iN nN sa); reflexivity. set B := Zo (Nint k) (fun z => forall i, i <=c z -> inc (di i) J). have oB: inc \0c B. have oo: inc \0c (Nint k) by apply/(NintP kN). by apply: (Zo_i oo) => i /cle0 ->; rewrite - j0v. have neB: nonempty B by ex_tac. have BI: sub B (Nint k) by apply:Zo_S. have BN:= (sub_trans BI (@Nint_S1 k)). have Bf:= (sub_finite_set BI (@finite_Nint k)). move:(finite_subset_Nat BN Bf neB) => [i1 i1B i1a]. have li1n: i1 <c n by apply: clt_leT lkn; move/(NintP kN): (BI _ i1B). have i1N:= (BN _ i1B). have la: forall i, i <=c i1 -> e (k -c i -c \1c) = di i. move => i ii; move:(NS_le_nat ii i1N) => iN. move: i iN ii; apply: Nat_induction. by rewrite (cdiff_n0 kN) la0. move => j jN Hr b1. set x := di (csucc j). have xJ: inc x J by apply: (Zo_hi i1B). have epx:=(Hr (cleT (cleS jN) b1)). have [a lak av]:= (jp5 _ xJ). have cjln:=(cle_ltT b1 li1n). have : x <c di j. rewrite - (div2 _ jN cjln); apply:(csum_M0lt (JN _ xJ) q0). rewrite av - epx => la. move /(NintP kN): (BI _ i1B) => lik1. move:(cle_ltT b1 lik1) => ltcjk. set b := (k -c csucc j) -c \1c. set c := (k -c j) -c \1c. have lb: c <c k. have ljk:=(cle_ltT (cleS jN) ltcjk). move:(cpred_pr (NS_diff j kN) (cdiff_nz ljk)) => [sa sb]. rewrite /c - (cpred_pr4 (CS_diff _ _)). apply/(cleSltP sa); rewrite - sb. apply:(cdiff_ab_le_a _ (CS_nat kN)). case: (cleT_el (proj31_1 lb) (proj31_1 lak) ) => lc. by move: (jp2 _ _ lc lak); move/(cltNge la). have bN: natp b by apply(NS_diff _ (NS_diff _ kN)). have bv1: csucc b = c by exact:(div0 _ _ jN kN ltcjk). have ld: a <=c b by apply/(cltSleP bN); rewrite bv1. case: (equal_or_not a b) => ee; first by rewrite - ee. have lab: a <c b by split. have lf: b <c c by rewrite - bv1; apply:(cltS bN). move:(jp1 _ _ lf lb); rewrite -/e epx => ra. have dijJ: inc (di j) J by rewrite - epx; exact: (jp4 _ lb). have su := (jp4 _ (clt_ltT lf lb)). move:(jp6 _ _ su dijJ ra). rewrite -(div2 j jN cjln) => /(csum_le2r qN (JN _ su) (diN (csucc j))) => t. by move:(jp1 _ _ lab (clt_ltT lf lb)); rewrite - av; move/(cleNgt t). have cp1: forall t, inc t E' -> t <c di i1. move => t tE; case: (NleT_el (diN i1) (EN _ tE)) => // h. move: (cdivision (EN _ tE) qN q0) => [QN RN [dvp rs]]. move:(csum_Meqlt (NS_prod qN QN) rs) ;rewrite - dvp => lta. have ltb:q *c (t %/c q) <=c t. by rewrite {2} dvp;apply:(Nsum_M0le _ (NS_prod qN QN)). have ltc: inc t (II (q *c (t %/c q))) by apply/(IIP _ (NS_prod qN QN)). move/setC_P: tE => [/(NintP qnN) ts /setU_P []]. have ltd: (t %/c q) <c n by apply/(cprod_lt2l qN QN nN); apply: cle_ltT ts. have xwx: t %/c q = (n -c (n -c csucc (t %/c q))) -c \1c. move /(cleSltP QN): ltd => sa. by rewrite (double_diff nN sa) -(cpred_pr4 (CS_succ _)) (cpred_pr2 QN). have lte: \1c <=c n -c i1 by apply/(cge1 (CS_diff n i1)) /(cdiff_nz li1n). have tJ: inc (q *c (t %/c q)) J. move: lta; rewrite - (cprod_nS _ QN) => lta; move:(cle_ltT h lta). move/(cprod_lt2l qN (ddN i1) (NS_succ QN))=>/(cltSleP QN) => H. move: (csum_Meqle i1 (csum_Meqle \1c H)). rewrite (cdiff_pr lte) (cdiff_pr (proj1 li1n)) (csumC \1c) - (Nsucc_rw QN). move => tt; rewrite xwx; apply:(Zo_hi i1B). by apply: (cdiff_Mle i1N (NS_succ QN)). exists (II (q *c (t %/c q))) => //;apply /funI_P; ex_tac. case: (equal_or_not i1 (cpred k)) => sa1. by left; move => t /cp1; rewrite (div _ li1n) sa1 - pkv. right. have lt1: csucc i1 <=c k by apply/(cleSltP i1N)/(NintP kN)/BI. have lt2: i1 <=c cpred k. by apply/(cleSSP (proj31_1 li1n) (CS_nat pkN)); rewrite - pkv. have lic : i1 <c cpred k by split. have lt3: csucc i1 <c k. by split => // h;move: (proj2 lic); rewrite - h; rewrite (cpred_pr2 i1N). have lci1n:=(clt_leT lt3 lkn). have Ha:= (cdiff_nz lci1n). have Hb: di i1 <> \0c by rewrite (div _ li1n); apply: (cprod2_nz q0). have Hc: inc (di i1) J by apply:(Zo_hi i1B _ (cleR (proj31 lt2))). case: (inc_or_not (di (csucc i1)) J) => Hd. have: inc (csucc i1) B. apply /Zo_P; split; first by apply/(NintP kN). move => i /cle_eqVlt; case; first by move ->. move /(cltSleP i1N); apply:(Zo_hi i1B). by move/i1a =>/(cltNge (cltS i1N)). move: (cpred_pr (diN i1) Hb) => []; set x := cpred (di i1) => xN xv. have He:inc x (Nint (q *c n)). apply /(NintP qnN); apply: (clt_leT (cltS xN)); rewrite - xv. rewrite (div _ li1n); exact:(cprod_Meqle _(cdiff_ab_le_a _ (CS_nat nN))). have ra: forall t, inc t E' -> t <=c x. by move => t tE; move: (cp1 _ tE); rewrite xv => /(cltSleP xN). have rb: inc x E'. apply /setC_P; split; first exact. move /setU_P => [s sa /funI_P [j ja jb]]; case: Hd. move: sa; rewrite jb; move /(IIP _ (JN _ ja)) => [hu hv]. have wa: j <c (di i1) by rewrite xv; apply/(cltSleP xN). move:(jp6 _ _ ja Hc wa); rewrite xv => sa. have: j +c q = di i1 by rewrite xv;apply:(cleA sa); apply/(cleSltP xN). by rewrite - (div2 _ i1N lci1n);move/(csum_eq2r qN (JN _ ja) (diN _))=> <-. move: (la _ (cleR (proj31 lt2))); rewrite xv. set j := k -c i1 -c \1c; move => ej1. have jv: j = k -c csucc i1 by rewrite /j (cdiffA kN i1N NS1) - (Nsucc_rw i1N). have ljk: j <c k. rewrite jv; apply: (cdiff_Mlt kN kN (proj1 lt3)). apply:(csum_M0lt kN (@succ_nz _)). have jv2: ((n -c k) +c j) = (n -c (csucc i1)). rewrite jv - {2} (cdiff_pr lkn) (cdiffA2 kN (NS_diff k nN) (proj1 lt3)). by rewrite csumC. have jv3: di i1 = (q *c ((n -c k) +c j)) by rewrite jv2 (div _ li1n). rewrite - xv in ej1. by exists j; rewrite - jv3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)