proposition: Lemma cprod_Meqlt_gen a b b': natp a -> b <c b' -> a <> \0c -> (a *c b) <c (a *c b').
proof: Proof. move => aN lbb anz. case: (finite_or_infinite (proj32_1 lbb)) => fb'. move/NatP: fb' => b'N; exact: (cprod_Meqlt aN b'N lbb anz). rewrite (cprod_inf7 aN anz fb'). case: (finite_or_infinite (proj31_1 lbb)) => fb. move/NatP: fb => bN; move: (NS_prod aN bN) => /NatP fp. exact: (clt_fin_inf fp fb'). by rewrite (cprod_inf7 aN anz fb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)