proposition: Lemma Exercise6_31_B x y: inc x F -> (inc y (f x) <-> inc y F /\ finite_set (y -s x)).
proof: Proof. move: Exercise6_31_i =>[or sr]. move => xF; split. move: (@Exercise1_23d2 r' x or); rewrite sr -/f => h yf. move /setC1_P: (h xF) => /proj1/Zo_S/setP_P; rewrite sr => fxF. have yF := (fxF _ yf). move/ (Exercise6_31_fP xF yF): yf => q; split => //. case: (finite_or_infinite_set (y -s x)) => // di. have ce: (x \cap (y -s x)) = emptyset. by apply/set0_P => t /setI2_P [tx /setC_P /proj2]. case: (finite_not_infinite_set emptyset_finite). by move: (q _ di (@sub_setC y x)); rewrite ce. move =>[yF etc]; apply /(Exercise6_31_fP xF yF) => [z iz zy ]. case: (finite_or_infinite_set (x \cap z)) => // fi. move: (finite_union2 (sub_finite_set (@setI2_2 z (y -s x)) etc) fi). have ee1: z \cap (x \cap y) = x \cap z. rewrite setI2_A (setI2_C z); set_extens t; first by case/setI2_P. by move => ta; apply: setI2_i => //; apply: zy; case/setI2_P: ta. have <-: z = z \cap (y -s x) \cup (x \cap z). rewrite - ee1- set_IU2r; set_extens t; last by case /setI2_P. move => tz; apply/setI2_P; split => //; move: (zy _ tz) => ty. case: (inc_or_not t x) => tx. by apply/setU2_P; right; apply: setI2_i. by apply/setU2_P; left; apply/setC_P. by move/finite_not_infinite_set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)