proposition: Lemma double_diff n p: natp n -> p <=c n -> n -c (n -c p) = p.
proof: Proof. move=> nN lepn. have pN:= (NS_le_nat lepn nN). exact: (cdiff_pr2 pN (NS_diff p nN) (cdiff_pr lepn)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)