proposition: Lemma cprod_Mle_square x: x <=cc x \times x.
proof: Proof. rewrite - cprod2_pr1 - cprod2cr - cprod2cl; set a := cardinal x. case: (equal_or_not a \0c) => anz. by rewrite anz cprod0r;apply: (cleR CS0). apply: (cprod_M1le (CS_cardinal x) anz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)