proposition: Lemma cprod_inf5 a b c: a <c c -> b <c c -> infinite_c c -> a *c b <c c.
proof: Proof. move => l1 l2 ic. move: (proj31_1 l1) (proj31_1 l2) => ca cb. move:(cmax_p1 ca cb) => [da db]. have dc:= (Gmax_S (p:=fun z => z <c c) cardinal_le l1 l2). case: (finite_or_infinite (proj31_1 dc)) => fd. move: (cle_fin_fin fd da) (cle_fin_fin fd db). move /NatP => aN /NatP bN. by apply: clt_fin_inf => //; apply /NatP; apply: NS_prod. exact (cle_ltT (cprod_inf4 da db fd) dc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)