proposition: Lemma cnext_prod 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. move: (cprod_Mlele cx cy); rewrite oprod_cardinal // csquare_inf //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)