proposition: Lemma BQ_int01_or_osr: order_on BQ_int01_order BQ_int01.
proof: Proof. set r := (induced_order BQ_order BQ_int01). move: BQor_sr BQor_tor => pa pb. have sr1: sub BQ_int01 (substrate BQ_order) by rewrite pa; apply: Zo_S. exact:(iorder_osr (proj1 pb) sr1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)