proposition: Lemma cdiff_pr2 a b c: natp a -> natp b -> a +c b = c -> c -c b = a.
proof: Proof. by move=> aN bN h; move: (cdiff_pr1 aN bN); rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)