proposition: Lemma finite_Nintcc a b: finite_set (Nintcc a b).
proof: Proof. apply/card_finite_setP. case: (p_or_not_p (a <=N b)) => h. rewrite card_Nintcc //; move: h => [aN bN _]; fprops. have ->: (Nintcc a b) = emptyset. apply/set0_P => t /Zo_hi [/Nat_order_leP [pa _ pc] /Nat_order_leP [_ pe pf]]. case: h; split => //; exact:cleT pc pf. rewrite cardinal_set0;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)