proposition: Lemma cnext_sum x y: inc x E -> inc y E -> inc (x +o y) E.
proof: Proof. move: iC => [cc _]. move=> /(cnextP cc) [xo cx] /(cnextP cc) [yo cy]. apply /(cnextP cc);split; first by fprops. rewrite osum_cardinal //. move: (csum_Mlele cx cy); rewrite csum_inf1 //; apply /infinite_setP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)