proposition: Lemma csum_inf6 a b: cardinalp a -> cardinalp b -> (infinite_c a \/ infinite_c b) -> a +c b = cmax a b.
proof: Proof. wlog: a b / b <=c a. move => HH ca cb; case (cleT_ee cb ca)=> le1; first by apply: HH. by move => h; rewrite (cmaxC ca cb) csumC; apply:HH => //;apply/or_comm. move => lba ca cb cm;rewrite (cmax_yx lba); apply:(csum_inf lba). case:cm => // bi; exact:(cle_inf_inf bi lba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)