proposition: Lemma cardinal_pairs_lt n: natp n -> cardinal (Zo (coarse Nat) (fun z => [/\ \1c <=c (P z), (P z) <c (Q z) & (Q z) <=c n])) = (binom n \2c).
proof: Proof. move=> nN; rewrite /coarse. set (E:= Nint1c n). set T:=Zo _ _. move: NS1 NS2 => oN tN. case: (p_or_not_p (\2c <=c n)); last first. case: (cleT_el CS2 (CS_nat nN)). by move=> h h'. move=> h _; rewrite binom_bad //. case: (emptyset_dichot T); first by move=> ->; rewrite cardinal_set0. move=> [p /Zo_P [a1 [a2 a3 a4]]];move: a3. by case: (clt2 (cle_ltT a4 h)) => ->; [move /clt0 | move => /(cleNgt a2) ]. move=> le2n. have cE: cardinal E = n by rewrite card_Nint1c. rewrite - (card_p_subsets nN tN cE). apply /card_eqP. exists (Lf (fun z=> (doubleton (P z) (Q z))) T (subsets_with_p_elements card_two E)). saw; apply: lf_bijective. move=> z /Zo_P [zp [le1p [lepq npq] leqn]]. move: (cleT lepq leqn) (cleT le1p lepq) => a1 a2. have pE: inc (P z) E by apply /Nint_ccP1. have qE: inc (Q z) E by apply /Nint_ccP1. apply: Zo_i; last by apply: cardinal_set2. by apply /setP_P; apply: sub_set2. move=> u v /Zo_P [] /setX_P [pu _ _] [_ lt1 _] /Zo_P [] /setX_P [pv _ _] [_ lt2 _] h. case: (doubleton_inj h); move=> [e1 e2]. apply: pair_exten =>//. by move: lt1;rewrite e1 e2; move => [/(cltNge lt2)]. move => y /Zo_P [] /setP_P yE cy2. have [a [b [p1 p2 aN bN]]]: exists a, exists b, [/\ a <c b, doubleton a b = y, natp a & natp b]. have: sub y Nat by apply: (sub_trans yE); apply: Nint_S. move /set_of_card_twoP: cy2 => [a [b [ab ->]]] yN. move: (yN _ (set2_1 a b))(yN _ (set2_2 a b)) => aN bN. case: (NleT_el aN bN); [ by exists a, b | by rewrite set2_C ;exists b, a]. exists (J a b); aw => //. apply: Zo_i; aw; first fprops. have: inc a E by apply: yE; rewrite -p2; fprops. have: inc b E by apply: yE; rewrite -p2; fprops. by move /(Nint_ccP1 NS1 nN) => [_ pb] /(Nint_ccP1 NS1 nN) [pc _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)