proposition: Theorem card_ltP a b: natp a -> natp b -> (a <c b <-> exists c, [/\ natp c, c <> \0c & a +c c = b]).
proof: Proof. move=> aN bN; split; first by apply:card_ltP1. move=> [c [cN cnz <-]] ;apply:csum_M0lt; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)