proposition: Lemma BZ_of_Z_inc x: intp (BZ_of_Z x).
proof: Proof. case: x; move => p /=. apply:BZ_of_nat_i;apply: nat_to_B_Nat. apply:BZm_of_nat_i; apply: NS_succ;apply: nat_to_B_Nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)