proposition: Lemma BZor_sr: substrate BZ_order = BZ.
proof: Proof. move: Nat_order_wor => [[or _] sr]; move: BZ_order_aux1 => s1. move: (proj1 (iorder_osr or s1)) => h1; move: (opp_osr h1) => [h2 h3]. by rewrite orsum2_sr // h3 sr; rewrite iorder_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)