proposition: Lemma cdiff_pr6 a b: natp a -> natp b -> (csucc a) -c (csucc b) = a -c b.
proof: Proof. by move => /CS_nat ca /CS_nat cb; apply:cdiff_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)