proposition: Lemma Exercise4_5a Y T k: cardinal Y = k -> cardinal T = k -> natp k -> sub T (union Y) -> disjoint_set Y -> (forall Z, inc Z Y -> small_set (T \cap Z)) -> (forall Z, inc Z Y -> singletonp (T \cap Z)).
proof: Proof. move => cY cT kN Tu ald als. pose f x:= select (fun z => inc x z) Y. have Ha x: inc x T -> inc x (f x) /\ inc (f x) Y. move => xT; apply: select_pr. move /setU_P: (Tu _ xT)=> [y ya yb]; ex_tac. move => a b /= aY xa bY xb; case: (ald a b aY bY) => // dab; empty_tac1 x. have awx: lf_axiom f T Y by move => a /Ha []. have Hb a b: inc a T -> inc b T -> f a = f b -> a = b. move => aT bT eq1; move: (Ha _ aT)(Ha _ bT)=> [qa qb][qc qd]. rewrite eq1 in qa qb. exact:(als _ qd a b (setI2_i aT qa) (setI2_i bT qc)). set g := (Lf f T Y). have tg: target g = Y by rewrite /g ;aw. have sg: source g = T by rewrite /g ;aw. have stgc:source g =c target g by rewrite sg tg cY cT. have fsg: finite_set (source g) by rewrite sg; apply /NatP; rewrite cT. have ig : injection g by apply: lf_injective => // a /Ha []. move: (bijective_if_same_finite_c_inj stgc fsg ig) => bg. move => Z ZY; apply/singletonP; split; last exact: (als _ ZY). rewrite - tg in ZY. move: (proj2 (proj2 bg) _ ZY) => [x];rewrite sg /g => xs; rewrite LfV// => ->. move: (proj1 (Ha _ xs)) => xz; exists x; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)