proposition: Lemma cprod_inf a b: b <=c a -> infinite_c a -> b <> \0c -> a *c b = a.
proof: Proof. move=> leba ia nzb. move:(cprod_Meqle a leba); rewrite (csquare_inf ia) => h. exact: (cleA h (cprod_M1le (proj32 leba) nzb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)