proposition: Lemma cprod_eq2l: a <> \0c -> a *c b = a *c b' -> b = b'.
proof: Proof. move=> naz eql. case: (NleT_ell bN b'N) =>// aux. by case: (proj2 (cprod_Meqlt aN b'N aux naz)). by case: (proj2(cprod_Meqlt aN bN aux naz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)