proposition: Lemma Exercise5_9l8 q n k J p (E':= union p) (e := nth_elt J) (e':= fun i => e i -c q *c i) (V:= Ex59_pos_in_J J k) (V' := fun x => x -c q *c (V x)) (T:= Nint (q *c (n -c k))): natp n -> natp q -> \0c <c q -> k <=c n -> Ex59_Jprop q n k J -> natp k -> \0c <c k -> Ex59_Cprop n q J k p -> [/\ forall x, inc x E' -> V x = k -> e'(k -c \1c) +c q *c k <=c x, forall x, inc x E' -> \0c <c (V x) -> (V x) <c k -> e'( (V x) -c \1c) +c q *c (V x) <=c x /\ x <c e'(V x) +c q *c (V x), forall x, inc x E' -> q *c (V x) <=c x, forall x, inc x E' -> x = q *c (V x) +c V' x & order_isomorphism (Lf V' E' T) (graph_on cardinal_le E') (graph_on cardinal_le T) ].
proof: Proof. move => nN qN qp lkn jP kN kp pP. move: (Exercise5_9l6 jP kN kp) => [ra rb rc rd re]. move: (Exercise5_9k2 kN jP) => [jp1 jp2 jp3 jp4 jp5]. move:(jP) =>[cJ JN _ _]. have qnN:= NS_prod qN nN. have knz :=(nesym (proj2 kp)). have ha: forall x, inc x E' -> V x <=c k. move => x _; apply: ra. have hb: forall x, inc x E' -> x <c q *c n. move => x /setU_P [y ya yb]. apply:(Exercise5_9l4 nN qN qp pP yb ya). have hb': forall x, inc x E' -> natp x. move => x /hb h; exact:(NS_lt_nat h qnN). 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 Ev: E' = (Ex59_compl n q J) by move: pP => [/Zo_S /partitionsP [[]]]. have qa j x: inc x E' -> inc j J -> j <c x -> j +c q <=c x. move => xu; move:(xu) => /setU_P [y xy yp] jJ [le1 _]. case: (cleT_el (CS_sum2 j q) (proj32 le1)) => // xa. move:xu;rewrite Ev => /setC_P [xb] []; apply /setU_P. exists (Nintcc j (j +c (q -c \1c))); last by apply/funI_P; ex_tac. by apply /(Ex59_interval_prop (JN _ jJ) qN qp). have qa'' x: inc x J -> inc x E' -> False. move=>xJ;rewrite Ev => /setC_P [xb] []; apply /setU_P. have cx:= (CS_nat(Nint_S1 xb)). exists (Nintcc x (x +c (q -c \1c))); last by apply/funI_P; ex_tac. move: (csum_Meqlt (JN _ xJ) qp); rewrite (csum0r cx) => la. apply /(Ex59_interval_prop (JN _ xJ) qN qp); split; fprops. have qa' j x: inc x E' -> inc j J -> x <=c j -> x <c j. move => xu jJ le1; split => // exj;rewrite exj in xu; case: (qa'' _ jJ xu). have hb'':= (jp4 _ lpkk). move:(Exercise5_9k4 qN nN lkn jP) => [jp7 jp8 jp9 jp10]. have hc: forall x, inc x E' -> V x = k -> e'(k -c \1c) +c q *c k <=c x. move => x xe; move/(rc _ (hb' _ xe)) => H; move:{H} (H _ hb'')=> ww. rewrite - cpk [in q *c k] pkv (cprod_nS _ pkN) csumA -(jp8 _ lpkk). exact: (qa _ _ xe hb'' ww). have e0J: inc (e \0c) J by apply: (jp4 _ kp). have hc'': forall x, inc x E' -> V x = \0c -> x <c e'\0c. move => x xe /rb h; rewrite /e' cprod0r (cdiff_n0 (JN _ e0J)). apply: (qa' _ _ xe e0J); apply:(h _ e0J). have hd: forall x, inc x E' -> \0c <c (V x) -> (V x) <c k -> e'( (V x) -c \1c) +c q *c (V x) <=c x /\ x <c e'(V x) +c q *c (V x). move => x xE la lb. move: (re x la lb); rewrite -/(V x); move => [qa1 qb1 qc1 qd1]. rewrite -(cpred_pr4 (proj32_1 la)). split; last by rewrite -(jp8 _ lb); exact:(qa' _ _ xE qa1 qb1). have lc:=(cpred_lt (NS_lt_nat lb kN) (nesym (proj2 la))). have [pvN pvv]:= (cpred_pr (NS_lt_nat lb kN) (nesym (proj2 la))). rewrite [in q *c _] pvv (cprod_nS _ pvN) csumA -(jp8 _ (clt_ltT lc lb)). exact:(qa _ _ xE qc1 qd1). have he: forall x, inc x E' -> q *c (V x) <=c x. move => x xE; move:(ha _ xE) => la. case: (equal_or_not (V x) k) => lb. move:(hc _ xE lb); rewrite lb; apply:cleT. apply:csum_Mle0; fprops. case: (equal_or_not (V x) \0c) => lc. by rewrite lc (cprod0r); apply:(cle0n (hb' _ xE)). have vp:=(card_ne0_pos (proj31 la) lc). apply:cleT(proj1(hd _ xE vp (conj la lb))). apply:csum_Mle0; fprops. have hf: forall x, inc x E' -> x = q *c (V x) +c V' x. by move => x xE; rewrite(cdiff_pr (he _ xE)). have hf': forall x, inc x E' -> natp (V' x). move => x /hb' xN; apply:(NS_diff _ xN). have prop2 x: inc x E' -> V x <> k -> V' x <c e' (V x). move => xE vzk;have ltvk :=(conj (ra x) vzk). have: q *c (V x) +c V' x <c q *c (V x) +c e' (V x). rewrite - (hf _ xE) csumC;case:(equal_or_not (V x) \0c) => vz. have w:=(hc'' _ xE vz). by rewrite vz cprod0r (csum0r (proj32_1 w)). exact: (proj2 (hd _ xE (card_ne0_pos (proj31 (ra x)) vz) ltvk)). exact:(csum_lt2l (NS_prod qN (NS_le_nat (ra x) kN)) (hf' _ xE) (jp7 _ ltvk)). have scV' x x': inc x E' -> inc x' E' -> x <c x' -> V' x <c V' x'. move => xE xE' lxx. move: (ra x) (ra x'); rewrite -/(V x) -/(V x') => lvk lvk'. move:(hb' _ xE)(hb' _ xE') => xN xN'. case: (equal_or_not (V x') \0c) => vz'. move/(rb x'): (vz') => lt1. case: (equal_or_not (V x) \0c) => vz. by rewrite /V' vz vz' cprod0r !cdiff_n0. have w: forall z, inc z J -> z <c x -> False. move => z zJ sa; case:(cltNge (clt_ltT sa lxx) (lt1 _ zJ) ). case: (equal_or_not (V x) k) => lv2. move /(rc x xN): lv2 => lv3; case: (w _ e0J (lv3 _ e0J)). have lv3:=(card_ne0_pos (proj31 lvk) vz). move: (re _ lv3 (conj lvk lv2)); rewrite -/(V x); move => [_ _ zJ zv]. case: (w _ zJ zv). have vzp':=(card_ne0_pos (proj31 lvk') vz'). case: (equal_or_not (V x) k) => vzk. move/(rc _ xN): (vzk) => lt1. case: (equal_or_not (V x') k) => vzk'. move: lxx; rewrite {1}(hf _ xE) {1} (hf _ xE') vzk vzk'. apply:(csum_lt2l (NS_prod qN kN) (hf' _ xE) (hf' _ xE')). move: (re _ vzp' (conj lvk' vzk')) => [sa sb _ _]. case:(cltNge (clt_ltT (lt1 _ sa) lxx) sb). have ltvk :=(conj lvk vzk). have sc := (NS_le_nat lvk kN). have sc' := (NS_le_nat lvk' kN). move:(cpred_pr sc' vz') => [v''N v''v]; have v'v:= (cpred_pr4(proj31 lvk')). have vx'1k: V x' -c \1c <c k. by rewrite - v'v; apply/(cleSltP v''N); rewrite -v''v. have qvN:=(NS_prod qN sc). have prop1: e' (V x' -c \1c) <=c V' x'. have sa: q *c (V x') +c e' (V x' -c \1c) <=c q *c (V x') +c V' x'. rewrite csumC - (hf _ xE'); case: (equal_or_not (V x') k) => vzk'. by move: (hc _ xE' vzk'); rewrite vzk'. exact: (proj1 (hd _ xE' vzp' (conj lvk' vzk'))). apply:(csum_le2l (NS_prod qN sc')(jp7 _ vx'1k) (hf' _ xE')) sa. case: (equal_or_not (V x) (V x')) => sv. move: lxx; rewrite {1} (hf _ xE) {1} (hf _ xE') - sv. exact:(csum_lt2l qvN (hf' _ xE) (hf' _ xE')). suff h: e' (V x) <=c e' (V x' -c \1c). exact:(clt_leT (clt_leT (prop2 _ xE vzk) h) prop1). apply: (jp9 _ _ _ vx'1k);rewrite -v'v; apply /(cltSleP v''N); rewrite -v''v. split; last exact. case:(equal_or_not (V x) \0c) => vz; first by rewrite vz; exact (proj1 vzp'). have vzp:=(card_ne0_pos (proj31 lvk) vz). case:(equal_or_not (V x') k) => vzk'; first by rewrite vzk'. case: (cleT_el (proj31 lvk) (proj31 lvk')) => // ll. move:(cpred_pr sc vz) => [vwN vwv]. have tt: V x' <=c cpred (V x) by apply /(cltSleP vwN); rewrite - vwv. case: (cleNgt (jp2 _ _ tt (cle_ltT (cpred_le (proj31 lvk)) ltvk))). move: (re _ vzp ltvk) (re _ vzp' (conj lvk' vzk')) => [_ _ _ td] [_ tb' _ _]. exact:(clt_leT (clt_ltT td lxx) tb'). have scV'' x x': inc x E' -> inc x' E' -> x <=c x' -> V' x <=c V' x'. move => xe xe' lexy; case: (equal_or_not x x') => lxx. rewrite lxx; apply: (cleR (CS_nat (hf' _ xe'))). exact (proj1 (scV' _ _ xe xe' (conj lexy lxx))). have iV': {inc E' &,injective V'}. move => x x' xE xE' /= sv. case: (NleT_ell (hb' _ xE)(hb' _ xE')) => // lxx. by case: (proj2(scV' _ _ xE xE' lxx)). by case: (proj2(scV' _ _ xE' xE lxx)). have ce': cardinal E' = q *c (n -c k). move: (pP) => [qa3 qb'' qc'']. move: (partition_nq_pr1 qa3); rewrite qb''. move/Zo_S: qa3 => /partitionsP [[ <-]] //. have np := (clt_leT kp lkn). have cN:= (NS_prod qN (NS_diff k nN)). have ax: lf_axiom V' E' T. move => t tE; apply /(NintP cN). set y := cpred (q *c n). have nnz := (nesym (proj2 np)). move:(cpred_pr qnN (cprod2_nz (nesym (proj2 qp)) nnz)) =>[yN yv]. have lety: t <=c y by move: (hb _ tE); rewrite yv; move/(cltSleP yN). have yE1:=(cpred_lt qnN (cprod2_nz (nesym (proj2 qp)) nnz)). case: (inc_or_not y E') => yE. have sa:V' y <c q *c (n -c k). case (equal_or_not (V y ) k) => eyk. move: yE1. rewrite -/y {1} (hf _ yE) eyk -{1} (cdiff_pr lkn) cprodDr => sa. exact: (csum_lt2l (NS_prod qN kN)(hf' _ yE) cN sa). exact:(clt_leT (prop2 _ yE eyk) (jp10 _ (conj (ha _ yE) eyk))). exact:(cle_ltT (scV'' _ _ tE yE lety) sa). move:(Exercise5_9l7 nN qN qp lkn jP kN kp); rewrite - Ev; case. by move/yE. case. move => h;apply: (cle_ltT (cdiff_ab_le_a _ (proj31 lety)) (h t tE)). move => [j [ja jb jc jd je]]. have jN:= (NS_lt_nat ja kN). have x'N := NS_prod qN (NS_sum (NS_diff k nN) jN). set x' := (q *c ((n -c k) +c j)) in ja jb jc jd x'N. move: (cpred_pr x'N jb) => [xN xv]. apply: (cle_ltT (scV'' _ _ tE jd (je _ tE))). apply/(cdiff_Mlt cN xN (he _ jd))/(cleSltP xN). rewrite -xv {1} /x' cprodDr; apply:csum_Meqle; apply:cprod_Meqle. case: (equal_or_not j \0c) => jnz. rewrite jnz; exact:(cle0x (proj31 (ha _ jd))). move: (cpred_pr jN jnz) => [ua ub]. have uc: cpred j <c j by rewrite {2} ub; fprops. have la : (cpred x') <=c e j by rewrite /e jc {2} xv; fprops. have: e (cpred j) <c e j by apply: jp1. have cpjJ :=(jp4 _(clt_ltT uc ja)). rewrite {2} /e jc {1} xv; move/(cltSleP xN); case/cle_eqVlt => lb. by case: (qa'' _ _ jd); rewrite - lb. rewrite -(Exercise5_9l6bis jP kN kp xN ja jnz lb la). apply:cleR. exact:(proj31 (ra (cpred x'))). have bo : bijection_prop (Lf V' E' T) E' T. saw. have fse:finite_set E' by apply /NatP; rewrite ce'. have ce'': cardinal E' = cardinal T by rewrite card_Nint. apply:bijective_if_same_finite_c_inj; aw; trivial; apply:lf_injective => //. have iso:order_isomorphism (Lf V' E' T) (graph_on cardinal_le E') (graph_on cardinal_le T). have sa: cardinal_set E' by move => t /hb' /CS_nat. move: (wordering_cle_pr sa) => [[or1 _] sr1]. have sb: cardinal_set T by move => t /Nint_S1 /CS_nat. move: (wordering_cle_pr sb) => [[or2 _] sr2]. clear sa sb; hnf; rewrite sr1 sr2; split => //. hnf; aw => x y xe ye; rewrite ! LfV//; move: (ax _ xe) (ax _ ye) => xt yt. split;move/graph_on_P1 => [_ _ lta]; apply/graph_on_P1; split => //. by apply: scV''. by case:(NleT_el (hb' _ xe)(hb' _ ye)) => // /(scV' _ _ ye xe) /(cleNgt lta). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)