proposition: Lemma cprod_inf6 a b: cardinalp a -> cardinalp b -> (infinite_c a \/ infinite_c b) -> a <> \0c -> b <> \0c -> a *c b = cmax a b.
proof: Proof. move => ca cb H anz bnz. case: (cleT_ee ca cb)=> le1. rewrite (cmax_xy le1). have ib: infinite_c b by case H => // h; move:(cle_inf_inf h le1). by rewrite cprodC (cprod_inf le1 ib anz). rewrite (cmax_yx le1). have ib: infinite_c a by case H => // h; move:(cle_inf_inf h le1). by rewrite (cprod_inf le1 ib bnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)