proposition: Lemma Exercise4_4 n E C: natp n -> cardinal E = n -> sub C (coarse E) -> (forall x y, inc x E -> inc y E -> x <> y -> (exactly_one (inc (J x y) C) (inc (J y x) C))) -> exists2 f, bijection_prop f (Nint1c n) E & (forall i, \1c <=c i -> i <c n -> inc (J (Vf f i) (Vf f (csucc i))) C).
proof: Proof. move=> nN cn _; move: n nN E cn C. apply: Nat_induction1. move=> n nN hrec E nE C cp. case: (emptyset_dichot E) => Ee. rewrite -nE Ee cardinal_set0. have ->: (Nint1c \0c) = emptyset. apply /set0_P => t /(Nint1cP NS0) [pa pb]. case: (clt0 (conj pb pa)). exists (identity emptyset); [by apply: identity_bp | by move => i _ /clt0]. move: Ee => [a aE]. set E1 := E -s1 a. have s1:sub (singleton a) E by apply: set1_sub. set Z1:= Zo E1 (fun z => inc (J z a) C). set Z2:= Zo E1 (fun z => inc (J a z) C). have Z1E1: sub Z1 E1 by apply: Zo_S. have sE1E: sub E1 E by apply: sub_setC. have Z1E: sub Z1 E by apply: sub_trans sE1E. have Z2E: sub Z2 E by apply: sub_trans sE1E=>//; apply: Zo_S. have Z2c: Z2 = E1 -s Z1. set_extens t. move /Zo_P => [ta tb]; apply /setC_P; split => //; move /Zo_P => [_ tc]. move /setC_P: ta => [te ] /set1_P tna. by case: (proj2 (cp _ _ te aE tna)). move => /setC_P [te h]; apply /Zo_P;split => //. move /setC_P: (te) => [te1 ] /set1_P tna. case: (proj1 (cp _ _ te1 aE tna)) => // pa. case: h; apply :Zo_i => //. move: (cardinal_setC s1); rewrite /cdiff cardinal_set1 -/E1 csumC. move: (cardinal_setC Z1E1); rewrite /cdiff -Z2c nE; move => <-. set n1:= cardinal Z1; set n2:= cardinal Z2. rewrite - (csucc_pr4 (CS_sum2 n1 n2))=> rel1. have n1n2N: natp (n1 +c n2). by move:nN; rewrite - rel1 => h;move:(NS_nsucc (CS_sum2 n1 n2) h). move: (cltS n1n2N); rewrite rel1 => aux2. have aux3: n1 <=c (n1 +c n2) by apply: csum_M0le; rewrite /n1; fprops. have aux4: n2 <=c (n1 +c n2) by apply: csum_Mle0; rewrite /n2;fprops. have ltn1n:= cle_ltT aux3 aux2. have ltn2n:= cle_ltT aux4 aux2. move:(NS_lt_nat ltn1n nN) (NS_lt_nat ltn2n nN)=> n1N n2N. have c1p: (forall x y, inc x Z1 -> inc y Z1 -> x <> y -> exactly_one (inc (J x y) C) (inc (J y x) C)). move=> x y xz1 yz1 xy; apply: (cp _ _ (Z1E _ xz1)(Z1E _ yz1) xy). have c2p: (forall x y, inc x Z2 -> inc y Z2 -> x <> y -> exactly_one (inc (J x y) C) (inc (J y x) C)). by move=> x y xz1 yz1 xy; apply: (cp _ _ (Z2E _ xz1)(Z2E _ yz1)). move: (hrec n2 ltn2n Z2 (refl_equal (cardinal Z2)) C c2p). move: (hrec n1 ltn1n Z1 (refl_equal (cardinal Z1)) C c1p). clear c1p c2p hrec aux2 aux3 aux4. move => [f1 [bf1 sf1 tf1] f1p][f2 [bf2 sf2 tf2] f2p]. pose f i := Yo (i = (csucc n1)) a (Yo (i <=c n1) (Vf f1 i) (Vf f2 (i -c (csucc n1)))). have lt1:= (cltS n1N). have p1: f (csucc n1) = a by rewrite /f; Ytac0. have p2: forall i, i <=c n1 -> f i = Vf f1 i. move=> i lei. by rewrite /f (Y_false (proj2(cle_ltT lei lt1))) (Y_true lei). have p3 i: (csucc n1) <c i -> f i = Vf f2 (i -c (csucc n1)). move=> [lesi nsi]; rewrite /f; Ytac0; Ytac in1 => //. case:(cltNge lt1 (cleT lesi in1)). have p4 i: i <> \0c -> i <=c n1 -> inc (f i) Z1. move=> inz in1; rewrite (p2 _ in1);rewrite -tf1; Wtac; try fct_tac. by rewrite sf1; apply /(Nint1cP n1N). have snN:= (NS_succ n1N). have nn12: n = ((csucc n1) +c n2) by rewrite csumC csum_nS // csumC rel1. have p5 i: csucc n1 <c i -> i <=c n -> inc (i -c (csucc n1)) (source f2). move=> [n1i ni3] n2i; rewrite sf2 ; apply /(Nint1cP n2N). move:(NS_diff (csucc n1)(NS_le_nat n2i nN)) (cdiff_pr n1i). set d := _ -c _ ; move=> sN sv; split. dneg dz; rewrite - sv dz; rewrite csum0r //; exact: (proj31 n1i). apply: (csum_le2l snN) => //; rewrite sv -nn12//. have p6 i: (csucc n1) <c i -> i <=c n -> inc (f i) Z2. move=> in1 lin; rewrite (p3 _ in1) -tf2; Wtac; fct_tac. set sf3 :=(Nint1c n). have ta i: inc i sf3 -> inc (f i) E. move=> /(Nint1cP nN) [inz lein]. have ci:= proj31 lein. have cn: cardinalp (csucc n1) by fprops. case: (cleT_el ci cn)=> aux1; last by apply: Z2E;apply: p6. case: (equal_or_not i (csucc n1)) => is1; first by rewrite is1 p1. have : i <c (csucc n1) by split. by move /(cltSleP n1N); move => lin1; apply: Z1E; apply: p4. set F := Lf f sf3 E. have sF: source F = sf3 by rewrite /F; aw. have tF: target F = E by rewrite /F; aw. have fF: function F by apply: lf_function. have fpF: function_prop F sf3 E by []. have injF: injection F. apply: lf_injective => // u v /(Nint1cP nN) [ua ub] /(Nint1cP nN) [va vb]. wlog: u v ua ub va vb / u <c v. move => H; case: (cleT_ell (proj31 ub) (proj31 vb)) => //. by apply: H. by move => lvu /esym sf; symmetry; apply: H. move => luv. case: (equal_or_not u (csucc n1)) => un1. rewrite un1 p1; rewrite un1 in luv; move:(p6 v luv vb) => /Zo_S /setC1_P. by case=> _ => h h'; case: h. case: (cleT_el (proj31 ub) (proj32_1 lt1)). move => h1; move/ (cltSleP n1N): (conj h1 un1) => h2. move: (p4 _ ua h2)=> h3. case: (equal_or_not v (csucc n1)) => vn1. by rewrite vn1 p1=> h4; move/Zo_S: h3 => /setC1_P[_]; case. case: (cleT_el (proj31 vb) (proj32_1 lt1)). move => h1'; move/ (cltSleP n1N): (conj h1' vn1) => h2'. rewrite (p2 _ h2)(p2 _ h2'). by apply: (proj2 (proj1 bf1)); rewrite sf1; apply/(Nint1cP n1N). move => h4 h5; move: (p6 v h4 vb); rewrite Z2c => /setC_P [_]; case;ue. move => h1; move:(clt_ltT h1 luv)=> h2; rewrite (p3 u h1) (p3 v h2)=> h3. move: (proj2 (proj1 bf2) _ _ (p5 u h1 ub) (p5 v h2 vb) h3) => h4. by rewrite - (cdiff_pr (proj1 h1)) - (cdiff_pr (proj1 h2)) h4. exists F. split => //. apply: bijective_if_same_finite_c_inj => //. by rewrite /F lf_source lf_target /sf3 nE card_Nint1c. by rewrite /F lf_source /sf3 /finite_set (card_Nint1c nN); apply /NatP. move=> i i1 lin. have inz: i <> \0c by move /cge1P: i1 => [_ /nesym]. move: (proj1 lin) => lein ;move: (NS_le_nat lein nN) => iN. have i3: inc i sf3 by apply /(Nint1cP nN). have si3: inc (csucc i) sf3. by apply /(Nint1cP nN); split; [ apply: succ_nz | apply /cleSltP]. rewrite /F LfV // LfV //. case: (cleT_el (proj31 lein) (CS_succ n1)) => aux1. case: (equal_or_not i (csucc n1)) => in1. have: inc (f (csucc i)) Z2. apply:p6; first by rewrite in1; apply: cltS. by apply/(cleSltP (NS_lt_nat lin nN)). by move/Zo_hi; rewrite in1 p1. have lein1: i <=c n1 by apply /(cltSleP n1N); split. case: (equal_or_not i n1) => eqin1. by move:(p4 _ inz lein1); rewrite eqin1 p1;move/Zo_hi. have sin1: (csucc i) <=c n1 by apply /cleSltP. by rewrite p2 // p2 //; apply: f1p. have p7:= (clt_leT aux1 (cleS iN)). rewrite p3 // p3 //. have aux1':= (proj1 aux1). move:(NS_diff (csucc n1) iN) (cdiff_pr aux1'). set k:= i -c (csucc n1); move => kN kp. have ->: (csucc i) -c (csucc n1) = csucc k. rewrite - csucc_diff // cdiff_pr6//. apply: f2p. apply: cge1; fprops. by move=> kz; case: (proj2 aux1); rewrite - kp kz (csum0r (CS_succ _)). by apply: (csum_lt2l snN) => //;rewrite kp -nn12. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)