proposition: Lemma strict_pos_P a: natp a -> (\0c <> a <-> \0c <c a).
proof: Proof. move => aN; split; [ move /nesym; apply:card_ne0_pos; fprops | by case ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)