proposition: Lemma Nint_co_cc p: natp p -> Nintc p = Nint (csucc p).
proof: Proof. move => pN;move:(NS_succ pN) => snP; rewrite (NintE snP);set_extens t. - by move => /(NintcP pN) /(NleP pN). - by move => /(NleP pN) /(NintcP pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)