proposition: Lemma eta_likeQps: eta_like BQps_order.
proof: Proof. rewrite /BQps_order. set r := (induced_order BQ_order BQps). move: BQor_sr BQor_tor cardinal_Q => sr' tor' cq. have sr1: sub BQps (substrate BQ_order) by rewrite sr'; apply:BQps_sBQ. move:(iorder_osr (proj1 tor') sr1)(total_order_sub tor' sr1); rewrite -/ r. move => [or sr] tor. move: cardinal_Qps => cq'. have pd: countable_set BQps by apply/countableP; rewrite cq' aleph0_pr1; fprops. have H: forall x y, glt r x y <-> (inc x BQps /\ x <q y). move => x y; split; move => [xs lxy]. by move/iorder_gleP: xs => [za zb /BQle_P zc]. move: lxy => [lxy nxy];split => //; apply/iorder_gle0P => //. move / qlt0xP: xs => ha1; apply / qlt0xP; BQo_tac. by apply /BQle_P. rewrite/eta_like /eta_like0 sr; split => //; split => //. + move => x xq; move: (BQhalf_pos xq)(BQhalf_pos1 xq) => qa qb. by exists (BQhalf x); apply/H. + move => x xq; exists (x +q \1q); apply/H; split => //. apply:(qlt_succ (BQps_sBQ xq)). + move => x y /H [xp /BQmiddle_comp [l1 l2]]. exists (BQmiddle x y); split; apply/H => //; split => //. move / qlt0xP: xp => ha1; apply / qlt0xP; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)