proposition: Lemma cdiff_pr3 a b n: natp n -> a <=c b -> b <=c n -> (n -c b) <=c (n -c a).
proof: Proof. move => mN le1 le2. have bN:=(NS_le_nat le2 mN). have aN:=(NS_le_nat le1 bN). have dN:=(NS_sum (NS_diff a bN) (NS_diff b mN)). rewrite - {2} (cdiff_pr le2) -{2} (cdiff_pr le1). rewrite - csumA (csumC a) (cdiff_pr1 dN aN); apply:(csum_Mle0 _ (CS_diff n b)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)