proposition: Lemma cdiff_pr8 n p q: q <=c p -> p <=c n -> natp n -> (n -c p) +c q = n -c (p -c q).
proof: Proof. move => leqp lepn nN. have pN := NS_le_nat lepn nN. have qN := NS_le_nat leqp pN. rewrite - {2} (cdiff_pr lepn) -{2} (cdiff_pr leqp) [in RHS] csumC. by rewrite csumA (cdiff_pr1 (NS_sum (NS_diff p nN) qN) (NS_diff q pN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)