proposition: Lemma zle_P x y: gle BZ_order x y <-> x <=z y.
proof: Proof. apply: (iff_trans (orsum2_gleP _ _ x y)). move: BZ_order_aux => [pa pb]. move: BZor_sr; rewrite orsum2_sr //; move => ->. split. move => [ra rb rc]; split => //; case: rc. move => [rd re] /opp_gleP => h; constructor 1;split => //. by move: (iorder_gle1 h) => /Nat_order_leP [_ _]. move => [rd re] /Nat_order_leP [_ _ rf]; constructor 3;split => //. case: (BZ_sgv ra) => //. case: (BZ_sgv rb) => //. by move => [rd re]; constructor 2;split => //;case: (BZ_sgv rb) => qv. move => [ra rb rc];split => //. move /candu2P: ra => [_ ra]; move /candu2P: rb => [_ rb]. have W := C1_ne_C0; have W' := C0_ne_C1. case: rc. move => [rd re rf]; constructor 1 ;split => //. case: ra; [move => [p1 _] | by move => [_]; rewrite rd]. case: rb; [move => [p2 _] | by move => [_]; rewrite re]. apply /opp_gleP; apply /iorder_gle0P => //. apply /Nat_order_leP; split => //. by case /setC1_P: p2. by case /setC1_P: p1. by move => [rd re]; constructor 3;split => //; rewrite re. move => [rd re rf]; constructor 2; rewrite rd re; split => //. case: ra; [ by move => [_]; rewrite rd | move => [p1 _] ]. case: rb; [ by move => [_]; rewrite re | move => [p2 _] ]. by apply /Nat_order_leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)