proposition: Lemma card_ltP1 a b: natp b -> a <c b -> exists c, [/\ natp c, c <> \0c & a +c c = b].
proof: Proof. move=> bN [ab nab]; move: (NS_diff a bN) => pa; exists (b -c a); split => //. by apply: cdiff_nz. by rewrite (cdiff_pr ab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)