proposition: Lemma cdiff_Mle a b c: natp a -> natp b -> c <=c (a +c b) -> (c -c b) <=c a.
proof: Proof. move=> aN bN cab. move: (NS_le_nat cab (NS_sum aN bN)) => cN. case: (NleT_ee cN bN) => cb. rewrite (cdiff_wrong cb); exact (cle0n aN). by apply: (csum_le2r bN (NS_diff b cN) aN); rewrite (cdiff_rpr cb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)