proposition: Lemma csum_inf a b: b <=c a -> infinite_c a -> a +c b = a.
proof: Proof. move=> leba ia; move :(leba) => [cb ca _]. apply: cleA; last by apply: csum_M0le. by rewrite - {2} (csum_inf1 ia); apply: csum_Meqle. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)