proposition: Lemma csucc_diff a b: natp a -> natp b -> (csucc b) <=c a -> a -c b = csucc (a -c (csucc b)).
proof: Proof. move=> aN bN aux; move: (NS_succ bN) => sN. apply: cdiff_pr2; fprops. have dN: natp (a -c (csucc b)) by fprops. by rewrite (csum_Sn _ dN) - (csum_nS _ bN); apply: cdiff_rpr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)