proposition: Lemma cdiffA a b c: natp a -> natp b -> natp c -> (b +c c) <=c a -> (a -c b) -c c = a -c (b +c c).
proof: Proof. move=> aN bN cN h. have aux:= (cdiff_pr h). apply: cdiff_pr2 =>//; first by fprops. symmetry; apply: cdiff_pr2; fprops. by rewrite - csumA csumC (csumC c b). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)