proposition: Lemma BZ_of_Z_le (x y: int): x <= y <-> ( (BZ_of_Z x) <=z (BZ_of_Z y)).
proof: Proof. have aux: forall (z:int), inc (BZ_of_Z z) BZp <-> 0 <= z. case => n. rewrite le0z_nat; split => // _; exact (positive_non_zero1 n). split => h. by move: (BZ_di_neg_pos (positive_non_zero2 n) h). discriminate h. apply: iff_sym. apply: (iff_trans (zle_diffP (BZ_of_Z_inc x) (BZ_of_Z_inc y))). by rewrite - BZ_of_Z_diff - Num.Theory.subr_ge0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)