proposition: Lemma eta_likeQp_int01: eta_like BQ_int01_order.
proof: Proof. rewrite /BQ_int01_order. set r := (induced_order BQ_order BQ_int01). move: BQor_sr BQor_tor cardinal_Q => sr' tor' cq1. have sr1: sub BQ_int01 (substrate BQ_order) by rewrite sr'; apply: Zo_S. move:(iorder_osr (proj1 tor') sr1)(total_order_sub tor' sr1); rewrite -/ r. move => [or sr] tor. have cq2:= cardinal_BQ_int01. have pd: countable_set BQ_int01 by apply/countableP; rewrite cq2 aleph0_pr1; fprops. have H: forall x y, glt r x y <-> [/\ \0q <q x, x <q y & y <q \1q]. move => x y; split. move => [ /iorder_gleP [/Zo_P [_ [ha _]] /Zo_P [_ [_ hb]] /BQle_P hc] hd]. by split. move => [ha [hb hc] hd]; split => //; apply/iorder_gleP; split. + apply/Zo_P; split; [rewrite -/(ratp x); BQo_tac | split => //; BQo_tac]. + apply/Zo_P; split; [rewrite -/(ratp y); BQo_tac | split => //; BQo_tac]. + by apply /BQle_P. rewrite/eta_like /eta_like0 sr; split => //; split => //. + move => x /Zo_P [xq [x0 x1]]. have xp: inc x BQps by apply/ qlt0xP. move: (BQhalf_pos xp)(BQhalf_pos1 xp) => qa qb. exists (BQhalf x); apply/H; split => //; by apply/ qlt0xP. + move => x /Zo_P [xq [x0 x1]]; move:(BQmiddle_comp x1) => [sa sb]. exists (BQmiddle x \1q); apply/H; split => //. + move => x y /H [xp /BQmiddle_comp [l1 l2] y1]. exists (BQmiddle x y); split; apply/H => //; split => //; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)