proposition: Theorem card_Nintcc a b: a <=N b -> cardinal (Nintcc a b) = csucc (b -c a).
proof: Proof. move=> [aN bN ab]. move: (cdiff_pr ab) (NS_diff a bN) => aux cN. have fb:= (proj41 (restr_plus_interval_is cN aN)). have eq: (Nintcc \0c (b -c a)) \Eq (Nintcc a b). exists (rest_plus_interval (b -c a) a); rewrite /rest_plus_interval. by hnf;rewrite lf_source lf_target; split => //; rewrite csumC aux. by rewrite -(card_Nintc cN); symmetry;apply /card_eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)