proposition: Lemma csum_inf5 a b c: a <c c -> b <c c -> infinite_c c -> a +c b <c c.
proof: Proof. move => l1 l2 ic. wlog lba: a b l1 l2 / b <=c a. move => h; case: (cleT_ee (proj31_1 l2) (proj31_1 l1)); first by apply:h. by rewrite csumC; apply:h. case: (finite_or_infinite (proj31_1 l1)) => ia; last by rewrite (csum_inf lba). move/NatP: ia => na; move/NatP:(NS_sum na (NS_le_nat lba na)) => fs. apply: (clt_fin_inf fs ic). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)