proposition: Lemma Sperner_15 U V (a:= cardinal U) (b := cardinal V): natp a -> natp b -> disjoint U V -> exists2 g, bijection_prop g (a+c b) (U \cup V) & Vfs g a = U.
proof: Proof. move => aN bN dj. move: (csum2_pr5 dj)=> cu. have /equipotent_ex_pr: a \Eq U by apply/card_eqP; rewrite double_cardinal. have /equipotent_ex_pr: b \Eq V by apply/card_eqP; rewrite double_cardinal. set gb := (equipotent_ex b V); set ga := (equipotent_ex a U). move =>[qa qb qc][qd qe qf]. pose g x := Yo (x <c a) (Vf ga x) (Vf gb (x -c a)). pose G := Lf g (a+c b) (U \cup V). have abN := (NS_sum aN bN). have sG: source G = a +c b by rewrite/G; aw. have saab: sub a (a +c b). move => t /(NltP aN) lta; apply/(NltP abN). apply:(clt_leT lta (csum_M0le b (CS_nat aN))). have saG: sub a (source G) by ue. have fga: function ga by fct_tac. have fgb: function gb by fct_tac. have ax: lf_axiom g (a +c b) (U \cup V). move => t tab; rewrite /g; Ytac lta. by apply: setU2_1; Wtac; rewrite qe; apply/NltP. move/(NltP abN): tab => tab. move: (NS_lt_nat tab abN) => tN. case: (NleT_el aN tN) => // leat. rewrite csumC in tab. apply: setU2_2; Wtac; rewrite qb; apply/(NltP bN); apply:cdiff_Mlt => //. have: bijection G. apply: bijective_if_same_finite_c_surj. rewrite /G; aw; rewrite (csum2_pr5 dj) - (csum2cl U) - (csum2cr _ V). rewrite card_card //; fprops. by rewrite/G; aw; apply finite_set_nat. apply: lf_surjective => //y; case/setU2_P. rewrite - qf => /(proj2 (proj2 qd)) [i]; rewrite qe => ia ->. by move: (saab i ia) => iab; ex_tac; rewrite /g Y_true//; apply/NltP. rewrite - qc => /(proj2 (proj2 qa)) [i]; rewrite qb => ia ->. move: (NS_inc_nat bN ia) => iN. have aux:~ i +c a <c a by apply:cleNgt;apply:(csum_Mle0 i (CS_nat aN)). have aux2: inc (i +c a) (a +c b). rewrite csumC; apply/(NltP abN). by apply: (csum_Meqlt aN); apply/(NltP bN). ex_tac; by rewrite /g Y_false // cdiff_pr1. have GU i: inc i a -> (Vf G i) = (Vf ga i). move => ia; rewrite /G/g LfV//; last by apply: saab. by rewrite /g Y_true//; apply/NltP. exists G; first by split => //;rewrite /G; aw. have fG: function G by fct_tac. set_extens t. move /(Vf_image_P fG saG) => [u ua ->];rewrite (GU _ ua); Wtac. rewrite - qf; move/(proj2 (proj2 qd)) => [i]; rewrite qe => ia ->. rewrite -(GU _ ia); apply /(Vf_image_P fG saG); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)