proposition: Lemma cdiffA2 a b c: natp a -> natp b -> c <=c a -> (a +c b) -c c = (a -c c) +c b.
proof: Proof. move => aN bN h. move:(NS_sum (NS_diff c aN) bN) (NS_le_nat h aN) => pa pb. rewrite - {1} (cdiff_pr h) - csumA (csumC c) cdiff_pr1 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)