proposition: Lemma positive_non_zero2bis p : inc (BZm_of_nat (nat_to_B p.+1)) BZms.
proof: Proof. exact: (positive_non_zero2 p). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)