proposition: Lemma BZ_of_Z_lt (x y:int): x < y <-> ( (BZ_of_Z x) <z (BZ_of_Z y)).
proof: Proof. rewrite Order.POrderTheory.lt_neqAle; split=> //. move/andP => [p1 /BZ_of_Z_le p2]; split => // eq. by move /eqP: p1; case; apply:BZ_of_Z_injective. case; move /BZ_of_Z_le => p1 p2; apply /andP; split => //. by apply /eqP => eq; case: p2; rewrite eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)