proposition: Lemma Exercise_6_1 E: infinite_set E <-> (forall f, function_prop f E E -> exists S, [/\ sub S E, nonempty S, S <> E & sub (Vfs f S) S]).
proof: Proof. split. move=> iE f [ff sf tf]. case: (emptyset_dichot E) => [ ee | [y yE]]. move/NatP: NS0; rewrite - cardinal_set0 - ee => fce. by case: (finite_not_infinite_set fce iE). have p1: (forall u, inc u E -> inc (Vf f u) E) by rewrite -{1} sf -tf; fprops. move:(induction_defined_pr (fun n => Vf f n) y). move: (integer_induction_stable yE p1). set g:=induction_defined _ _; set (F:= target g). move=> stg [sg sjg g0 gs]. have fg: function g by fct_tac. have yF: inc y F. rewrite -g0;apply: Vf_target => //; rewrite sg; apply:NS0. have sFf:sub F (source f) by ue. have fF: (sub (Vfs f F) F). move=> t /(Vf_image_P ff sFf) [u uF ->]. move: ((proj2 sjg) _ uF); rewrite sg; move => [n ns ->]. by rewrite -gs//;apply:Vf_target;[ fct_tac |rewrite sg; apply: NS_succ]. set (G:=Vfs f F). have sgg: sub (Vfs f G) G. have aux:sub (Vfs f F) (source f) by apply: (@sub_trans F). move=> t /(Vf_image_P ff aux) [u ui ->]; apply /(Vf_image_P ff sFf). exists u;fprops. exists G; split => //; first by apply: (@sub_trans F) =>//. exists (Vf f y); apply /(Vf_image_P ff sFf); ex_tac. move=> GE; move: yE; rewrite -GE;move=> /(Vf_image_P ff sFf)[u uF Wu]. move: ((proj2 sjg) _ uF) => [x0 x0g Wx]. rewrite sg in x0g; move: Wu; rewrite Wx -gs //. set (k:= csucc x0). move=> Wy. have kN: natp k by apply: NS_succ. have rec1: (forall i, natp i -> Vf g i = Vf g (i +c k)). have ck: cardinalp k by fprops. apply: Nat_induction; first by rewrite csum0l //g0 Wy. move => n nN; rewrite (gs _ nN) (csumC (csucc n) _) csum_nS //. move ->; rewrite csumC gs //; fprops. have rec2: (forall i, natp i -> forall j, natp j -> Vf g i = Vf g (i +c (j *c k))). move => i iN; apply: Nat_induction. rewrite cprodC cprod0r csum0r //; fprops. move=> n nN; rewrite (cprodC (csucc n) _) cprod_nS // csumA. rewrite cprodC -rec1 //; fprops. have rec4: (forall z, inc z E -> exists2 m, m <c k & z = Vf g m). move=> z; rewrite -GE;move=> /(Vf_image_P ff sFf) [w w1 w2]. move: ((proj2 sjg) _ w1) => [x xsg w3]. rewrite sg in xsg;move: w2; rewrite w3 -gs //; move => ->. have sxN: (natp (csucc x)) by fprops. have knz: (k <> \0c) by apply: succ_nz. move: (cdivision sxN kN knz) => [qN rN [pa pb]]. rewrite pa; exists (csucc x %%c k) => //; rewrite csumC cprodC -rec2 //. have sisg: sub k (source g) by rewrite sg; apply: (NS_inc_nat kN). have sEi: (sub E (Vfs g k)). move=> t tE; move: (rec4 _ tE) => [m /(NltP kN) ml ->]. apply /(Vf_image_P fg sisg); ex_tac. have fsi: (finite_set k) by apply: finite_set_nat. move: (finite_image_by fg fsi) => fs2. move: (sub_finite_set sEi fs2) => fs3. case: (finite_not_infinite_set fs3 iE). move=> h; case: (finite_or_infinite_set E) => //. rewrite /finite_set; set (n:= cardinal E); move /NatP => nN. have:(n \Eq E) by apply /card_eqP; rewrite /n double_cardinal. move=> [y [bjy sy ty]]. case: (emptyset_dichot E) => neE. have fpi: (function_prop (identity E) E E). saw; apply: identity_f. move: (h _ fpi) => [F [FE [t tF] _]];empty_tac1 t. have nz: n <> \0c by apply: card_nonempty1. set (f:= fun i => (csucc i) %%c n). have Ha: forall i, natp i -> inc (i %%c n) n. by move=> i iN; apply /(NltP nN); move: (cdivision iN nN nz) => [_ _ [_]]. have Hb:sub n Nat by apply:(NS_inc_nat nN). have Hc:(forall i, inc i n -> inc (f i) n). by move=> i iI; apply: Ha; apply: NS_succ; apply: Hb. move: (inverse_bij_fb bjy). move: (ifun_s y) (ifun_t y). rewrite sy ty;set x := (inverse_fun y) => sx tx bx. have fx: function x by fct_tac. have fy: function y by fct_tac. set (g:= fun u => Vf y (f (Vf x u))). have ta: (lf_axiom g E E). rewrite /g -{1} sx -ty; move=> t tsx /=; apply: Vf_target =>//. rewrite sy;apply: Hc; rewrite -tx; Wtac. set (g1:= Lf g E E). have fg1: (function g1) by apply: lf_function. have fpg1: function_prop g1 E E by split => //; rewrite /g1; aw. move: (h _ fpg1) => [F [FE [u uF] nFE Fsg]]. set (i:= Vf x u). have iin: inc i n by rewrite/i; Wtac; rewrite sx; apply: FE. have iN:= (Hb i iin). have WiF: inc (Vf y i) F. rewrite /i; move: (FE _ uF); rewrite -ty => uty. by rewrite (inverse_V bjy uty). have Hd: (forall j, natp j -> inc (Vf y ( (i +c j) %%c n)) F). apply: Nat_induction. rewrite Nsum0r //. have dp:(cdivision_prop i n \0c i). split; first by rewrite cprod0r Nsum0l //. by apply /(NltP nN). by move: (cquorem_pr iN nN NS0 iN dp) => [_ ] <-. move => m mN. have imN: natp (i +c m) by fprops. set (v:= (i +c m) %%c n) => WvF. have vN: natp v by rewrite /v; fprops. have : (inc (Vf g1 (Vf y v)) F). have aux: sub F (source g1) by rewrite /g1;aw. apply: Fsg; apply /(Vf_image_P fg1 aux); ex_tac. rewrite /g1 LfV//; last (by apply: (FE _ WvF)); rewrite /g. move: (Ha _ (NS_sum iN mN)); rewrite - {2} sy -/v => vs. rewrite (inverse_V2 bjy vs). have <-: ((csucc v) %%c n = (i +c (csucc m)) %%c n) => //. rewrite -/(eqmod _ _ n) (csum_nS _ mN); apply: (eqmod_succ nN nz vN imN). by rewrite /v /eqmod; symmetry; apply: eqmod_rem. case: nFE; apply: extensionality => //. rewrite -ty; move=> t tE. move: (bjy) => [_ sjy]. move: ((proj2 sjy) _ tE) => [v vsy ->]. move: vsy; rewrite sy => /(NltP nN) vn. move: iin => /(NltP nN) [lein _]. move: (f_equal (fun z => (z +c v)) (cdiff_pr lein)). move: (vn) => [len _ ]; move: (NS_le_nat len nN) => vB. rewrite - csumA; set k:= _ +c v => aux. have kb: natp k by rewrite /k; fprops. have dp:(cdivision_prop (i +c k) n \1c v) by split=> //; rewrite cprod1r;fprops. move: (cquorem_pr (NS_sum iN kb) nN NS1 vB dp) => [_ ] ->. by apply: Hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)