proposition: Lemma card_Nintcc_alt a b: a <=N b -> cardinal (Nintcc a b) = csucc (b -c a).
proof: Proof. move=> [aN bN ab]. have ca := (CS_nat aN). have H0: (Nintcc a a) = singleton a. apply: set1_pr. apply/(Nint_ccP1 aN aN); split; apply:(cleR ca). by move => v /(Nint_ccP1 aN aN) [va vb]; apply: cleA. have H1 n: natp n -> (Nintcc a (csucc (a +c n))) = (Nintcc a (a +c n))+s1 (csucc (a +c n)). move => nN; move: (NS_sum aN nN) => sN; move: (NS_succ sN) => ssN. set_extens t. move/(Nint_ccP1 aN ssN) =>[aet]; case/cle_eqVlt; first by move->; fprops. by move/(cltSleP sN) => ti; apply:setU1_r; apply/(Nint_ccP1 aN sN). case/setU1_P. move/(Nint_ccP1 aN sN)=>[sa sb]; apply/(Nint_ccP1 aN ssN); split => //. exact: (cleT sb (cleS sN)). move ->;apply/(Nint_ccP1 aN ssN); split => //. exact: (cleT (csum_M0le n ca) (cleS sN)). by apply/(cleR (CS_nat ssN)). have H2 n: natp n -> ~ inc (csucc (a +c n)) (Nintcc a (a +c n)). move => nN; move: (NS_sum aN nN) => sN. by move /(Nint_ccP1 aN sN) /proj2; apply:cltNge; apply:cltS. move: (cdiff_pr ab) (NS_diff a bN) => {2} <- cN. move: (b-c a) cN; clear b bN ab. apply: Nat_induction; first by rewrite (csum0r ca) H0 succ_zero cardinal_set1. move => n nN Hrec. by rewrite (csum_nS _ nN) (H1 _ nN) (csucc_pr (H2 _ nN)) Hrec. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)