proposition: Lemma positive_non_zero2 p : inc (BZm_of_nat (csucc (nat_to_B p))) BZms.
proof: Proof. apply: BZm_of_natms_i; first by apply: NS_succ;apply: nat_to_B_Nat. apply: succ_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)