proposition: Lemma cdiff_pr9 n p q: natp n -> natp p -> natp q -> q <=c p -> (n <=c p -c q <-> n +c q <=c p).
proof: Proof. move => nN pN qN lqp. rewrite - {2} (cdiff_pr lqp) csumC; split => h; first by apply:csum_Meqle. apply:(csum_le2l qN nN (NS_diff _ pN) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)