proposition: Lemma finite_Nint a: finite_set (Nint a).
proof: Proof. have aux:sub (Nint a) (Nintcc \0c a). by move => t /Zo_P [pa [pb [pc _]]]; apply /Zo_P. apply: (sub_finite_set aux (finite_Nintcc \0c a)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)