proposition: Lemma cprod_eq1 a b: cardinalp a -> cardinalp b -> a *c b = \1c -> (a = \1c /\ b = \1c).
proof: Proof. move => ca cb eq. case: (equal_or_not a \0c) => az. by move: eq; rewrite az cprod0l => bad; case: card1_nz. case: (equal_or_not b \0c) => bz. by move: eq; rewrite bz cprod0r => bad; case: card1_nz. case: (equal_or_not a \1c) => px1; first by rewrite - {2} eq px1 (cprod1l cb). move: (cprod_Mlele (cge2 ca az px1) (cge1 cb bz)). by rewrite (cprod1r CS2) eq => /(cltNge clt_12). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)