proposition: Lemma eta_likeQ: eta_like BQ_order.
proof: Proof. move: BQor_sr BQor_tor cardinal_Q => pa pb pc. have pd: countable_set BQ by apply/countableP; rewrite pc aleph0_pr1; fprops. rewrite/eta_like /eta_like0 pa; split => //; split => //. + move => x xQ; exists (x -q \1q); apply/BQlt_P. move:(BQsum_Mps (QS_diff xQ QS1) QpsS1). by rewrite - (BQdiff_sum_comm xQ QS1 QS1) BQsumC (BQdiff_sum QS1 xQ). + move => x xQ; exists (x +q \1q); apply/BQlt_P. apply:(BQsum_Mps xQ QpsS1). + move => x y /BQlt_P /BQmiddle_comp [l1 l2]. by exists (BQmiddle x y); split; apply/BQlt_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)