proposition: Lemma positive_non_zero1 p : inc (BZ_of_nat (nat_to_B p)) BZp.
proof: Proof. by apply:BZ_of_natp_i; apply:nat_to_B_Nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)