proposition: Lemma BQor_tor: total_order BQ_order.
proof: Proof. split; first by apply: BQor_or. move => x y; rewrite BQor_sr => xq yq. move/BQ_P: (xq) => [_ pax /BZps_sBZ pbx _]. move/BQ_P: (yq) => [_ pay /BZps_sBZ pby _]. case:(zleT_ee (ZSp pax pby)(ZSp pbx pay)) => h. by left; apply/BQle_P. by right; apply/BQle_P; split => //; red; rewrite BZprodC (BZprodC (Q y)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)