proposition: Lemma cprod_eq2lx a b b': natp a -> cardinalp b -> cardinalp b' -> a <> \0c -> a *c b = a *c b' -> b = b'.
proof: Proof. move=> aN cb cb' naz eql. wlog: b b' cb cb' eql / b <=c b'. move => H; case: (cleT_ee cb cb'); first by apply: H. move => bb'; symmetry; apply: H => //. move => lebb. case: (finite_or_infinite cb') => fb'. move/NatP: fb' => b'N; apply:(cprod_eq2l aN (NS_le_nat lebb b'N) b'N naz eql). case: (finite_or_infinite cb) => fb. move:(cprod_inf7 aN naz fb'); rewrite - eql => ha. rewrite - ha in fb'. have fb'': finite_c (a *c b) by apply/NatP; fprops. case:(finite_not_infinite fb'' fb'). by rewrite -(cprod_inf7 aN naz fb') -(cprod_inf7 aN naz fb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)