proposition: Lemma cardinal_pairs_le n: natp n -> cardinal(Zo (coarse Nat) (fun z=> [/\ \1c <=c (P z), (P z) <=c (Q z) & (Q z) <=c n])) = (binom (csucc n) \2c).
proof: Proof. move=> nN. rewrite (binom_2plus0 nN). rewrite - cardinal_pairs_lt // /coarse. set E1 := Zo _ _; set E2 := Zo _ _. have s21: sub E2 E1. move=> t /Zo_P [pa [pb [pc _] pd]]; apply: Zo_i => //. rewrite -(cardinal_setC s21). suff: (E1 -c E2 = n) by move => ->. set (T:= Nintcc \1c n). have ->: n = cardinal T by rewrite card_Nint1c. apply /card_eqP. exists (Lf P (E1 -s E2) T); hnf;saw. have cp: forall x, inc x (E1 -s E2) -> P x = Q x. move=> x /setC_P [] /Zo_P [xp [le1 le2 ne]] h. ex_middle npq; case: h; apply: Zo_i => //. apply: lf_bijective. move=> x xc; move: (cp _ xc). move: xc => /setC_P [] /Zo_P [xp [le1 le2 le]] ns h. apply /(Nint_ccP1 NS1 nN); split => //; ue. move => u v uc vc; move: (cp _ vc) (cp _ uc) => h1 h2. move: uc vc => /setC_P [] /Zo_P [] /setX_P [pu _ _] _ _ /setC_P [] /Zo_P [] /setX_P [pv _ _] _ _ sp. by apply: pair_exten => //; rewrite - h1 -h2 sp. move=> y => /(Nint_ccP1 NS1 nN) [l1y lyn]. have yN:= NS_le_nat lyn nN. exists (J y y); aw => //; apply /setC_P; split. apply: Zo_i; [ fprops | aw;split;fprops]. by move /Zo_hi => [_ [_ bad] _]; case: bad; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)