proposition: Lemma Exercise5_2 E: finite_set E -> nonempty E -> (even_card_sub E) \Eq (odd_card_sub E).
proof: Proof. move => fse nne. set n := cardinal E. pose ce := complement E. have cs1: forall X, sub (ce X) E by move => X; apply: sub_setC. have ce2: forall X, sub X E -> cardinal X +c cardinal (ce X) = n. by move => x xe; rewrite csum2cr csum2cl - cardinal_setC2. have fsx: forall X, sub X E -> natp (cardinal X). move => x xe; apply /NatP; apply: (sub_finite_set xe fse). have cs3: forall X, natp (cardinal (ce X)) by move => X; apply: fsx. have cs4: forall X, sub X E -> ce (ce X) = X. by move => X; apply:setC_K. have nN: natp n by move: fse => /NatP. case: (p_or_not_p (evenp n)) => ece; last first. have oddn: oddp n by split. exists (Lf ce (even_card_sub E) (odd_card_sub E)). saw; apply: lf_bijective. - move => c /Zo_P [] /setP_P cee evc; apply /Zo_P;split => //. by apply /setP_P. split; [by apply: cs3 | move => cxe; case: (proj2 oddn)]. by move:(csum_of_even evc cxe); rewrite (ce2 _ cee). - move => u v /Zo_P [] /setP_P uE _ /Zo_P [] /setP_P vE _ /(f_equal ce). by rewrite (cs4 _ uE) (cs4 _ vE). - move => y => /Zo_P [] /setP_P ye yo. move: (cs1 y) => xe; rewrite - (cs4 _ ye); exists (ce y)=> //. apply: Zo_i; [by apply /setP_P | ex_middle ceo1]. by case: ece; rewrite - (ce2 _ ye); apply:(csum_of_odd yo). have ce_e: forall X, sub X E -> evenp (cardinal X) -> evenp (cardinal (ce X)). move=> X XE ecx; ex_middle ceo1. by move:(proj2 (csum_of_even_odd ecx (conj (cs3 X) ceo1)));rewrite (ce2 _ XE). move: (rep_i nne); set t:= rep E=> repe. pose ut x := Yo (inc t x) (x -s1 t) (x +s1 t). have uut: forall x, sub x E -> (ut (ut x)) = x. move => x xE; rewrite /ut; case: (inc_or_not t x) => tx; Ytac0. have nst: ~(inc t (x -s1 t)) by move /setC1_P => []. by Ytac0; rewrite setC1_K. have nst: inc t (x +s1 t) by apply :setU1_1. by Ytac0; apply /setU1_K. have u1: forall x, sub x E -> sub (ut x) E. move => x xe s; rewrite /ut; Ytac st. by move => /setC_P [sx _]; apply: xe. by case /setU1_P; [ apply: xe | move => -> ]. exists (Lf (fun z => ut (ce z)) (even_card_sub E) (odd_card_sub E)). saw; apply: lf_bijective. - move => s => /Zo_P [] /setP_P ta tb; apply /Zo_P; split. apply /setP_P; fprops. move: (ce_e _ ta tb) => ec; move:(fsx _ (u1 _ (cs1 s))). rewrite /ut; Ytac xt => cb. by apply/(succ_of_oddP cb); rewrite - (csucc_pr2 xt). by move:(succ_of_even ec); rewrite (csucc_pr xt). - move => u v /Zo_P [] /setP_P ue _ /Zo_P [] /setP_P ve _ /(f_equal ut). by rewrite (uut _ (cs1 _)) (uut _ (cs1 _)) => /(f_equal ce); rewrite !cs4. - move => y => /Zo_P [] /setP_P ta tb; move: (u1 _ ta) => ue. exists (ce (ut y)) => //; last by rewrite (cs4 _ ue) (uut _ ta). apply: Zo_i; [by apply /setP_P | apply: (ce_e _ ue) ]. move: (fsx _ ue); rewrite /ut; Ytac xt => cb. by apply/(succ_of_evenP cb); rewrite - (csucc_pr2 xt). by move:(succ_of_odd tb); rewrite (csucc_pr xt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)