proposition: Lemma cdiff_Mlt' a b c: natp a -> natp b -> a <> \0c -> c <c (a +c b) -> (c -c b) <c a.
proof: Proof. move=> aN bN anz cab. move: (NS_lt_nat cab (NS_sum aN bN)) => cN. case: (NleT_ee cN bN) => cb. by rewrite (cdiff_wrong cb); apply/(strict_pos_P1 aN). by apply: (csum_lt2r bN (NS_diff b cN) aN); rewrite (cdiff_rpr cb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)