proposition: Lemma zle_P0 x y: x <=z y <-> [\/ [/\ inc x BZms, inc y BZms & (BZ_val y) <=c (BZ_val x)], [/\ inc x BZms & inc y BZp] | [/\ inc x BZp, inc y BZp & (BZ_val x) <=c (BZ_val y)]].
proof: Proof. split. move => h; move:(h) => [pa pb _]. case /BZ_i0P: pa => ha; case /BZ_i0P: pb => hb. by constructor 1 ;split => //; move /(zle_P3 ha hb): h. by constructor 2; split => //. by move: (zle_pr4 ha hb) => hc. by constructor 3;split => //; move /(zle_P1 ha hb): h. case; first by move => [pa pb pc]; apply /zle_P3. by move => [pa pb]; exact: (proj1 (zle_pr2 pb pa)). by move => [pa pb pc]; apply /zle_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)