proposition: Lemma BQor_or: order BQ_order.
proof: Proof. have ->:BQ_order = graph_on BQ_le BQ. apply: sgraph_exten => //. by move => t /Zo_P [] /setX_P []. by move => t /Zo_P [] /setX_P []. move => u v; split => /graph_on_P1 [pa pb pc]; apply /graph_on_P1 => //. apply: order_from_rel; split. - apply: qleT. - apply:qleA. - by move => x y [xQ yQ _]; split; apply:qleR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)