proposition: Lemma csum_eq2l: a +c b = a +c b' -> b = b'.
proof: Proof. move=> eql. case: (NleT_ell bN b'N) =>// aux. by case: (proj2 (csum_Meqlt aN aux)). by case: (proj2 (csum_Meqlt aN aux)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)