proposition: Lemma cdiff_pr1_gen a b: cardinalp a -> cardinalp b -> (finite_c b \/ b <c a) -> (a +c b) -c b = a.
proof: Proof. move => ca cb h. case: (finite_or_infinite ca). move /NatP => fa; apply: cdiff_pr1 => //; case: h; first by move /NatP. move => pa;apply: (NS_lt_nat pa fa). move => ica. have ba : b <c a by case: h => //; move => hh; apply: clt_fin_inf. by rewrite (csum_inf (proj1 ba) ica) cdiff_inf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)