proposition: Lemma BZdvdorder_or: order BZdvdorder.
proof: Proof. have aux: forall t, inc t BZps -> [/\ inc t BZ, inc t BZp & t <> \0z]. move => t /BZps_iP [h unz]; split => //; exact (BZp_sBZ h). apply: order_from_rel1. move => y x z pa pb; apply: (BZdvds_trans pb pa). move => u v pa pb d1 d2. move: (BZdvds_monotone pa d2)(BZdvds_monotone pb d1) => l1 l2; BZo_tac. move => u h; move: (aux _ h) => [uz _ unz]. exact (proj1 (BZdvd_itself uz unz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)