proposition: Lemma cprod_inf4 a b c: a <=c c -> b <=c c -> infinite_c c -> a *c b <=c c.
proof: Proof. move=> ac bc ci. wlog lab: a b ac bc / a <=c b. move => H; case: (cleT_ee (proj31 ac) (proj31 bc)) => ab; first by apply: H. by rewrite cprodC; apply: H. case: (Nat_dichot (proj31 bc)) => fc. apply: (Nat_le_infinite (NS_prod (NS_le_nat lab fc) fc) ci). move: (cprod_inf1 lab fc); rewrite cprodC => h; exact:(cleT h bc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)