proposition: Lemma zle_P6 x y: inc x BZm -> inc y BZm -> (x <=z y <-> (BZ_val y) <=c (BZ_val x)).
proof: Proof. case /setU1_P => xnz; case /setU1_P => ynz. - apply /(zle_P3 xnz ynz). - rewrite ynz BZ0_val; split. move => _; move: (BZ_valN (BZms_sBZ xnz)) => /cle0n xn //. by move /zgt0xP: xnz => [pa _ ]. - rewrite xnz; split. by move/zle0xP => h; case:(BZ_di_neg_pos ynz h). rewrite BZ0_val => pc; move /indexed_P: ynz => [_] /setC1_P [pa pb] _. case: pb; exact (cle0 pc). - rewrite xnz ynz BZ0_val;move :ZS0 =>h; split=> _; fprops; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)