proposition: Lemma Z_of_BZ_pb p : Z_of_BZ (BZ_of_Z p) = p.
proof: Proof. exact: (BZ_of_Z_injective (Z_of_BZ_pa (BZ_of_Z_inc p))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)