proposition: Lemma cdiff_ltb a b: natp b -> a <=c b -> a <> \0c -> b -c a <c b.
proof: Proof. move => bN leab anz. split; first by apply: (cdiff_ab_le_a _ (CS_nat bN)). move => dd; move:(proj2 (csum_M0lt bN anz)); rewrite csumC; case. by move: (cdiff_pr leab); rewrite dd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)