proposition: Lemma csum_inf2 a b c: cardinalp c -> infinite_c a -> b <c a -> a = b +c c -> a = c.
proof: Proof. move => cc ica lba sv. case: (cleT_el (proj32_1 lba) cc) => lac. by apply:(cleA lac); rewrite sv; apply:csum_Mle0. by case: (proj2(csum_inf5 lba lac ica)); rewrite - sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)