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