proposition: Lemma cdiff_Mlt a b c: natp a -> natp c -> b <=c c -> c <c (a +c b) -> (c -c b) <c a.
proof: Proof. move=> aN cN bc cab. move: (NS_le_nat bc cN) => bN. by apply: (csum_lt2r bN (NS_diff b cN) aN); rewrite (cdiff_rpr bc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)