proposition: Lemma BQps_or_osr: order_on BQps_order BQps.
proof: Proof. set r := (induced_order BQ_order BQps). move: BQor_sr BQor_tor => pa [pb _]. have sr1: sub BQps (substrate BQ_order) by rewrite pa; apply:BQps_sBQ. exact:(iorder_osr pb sr1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)