proposition: Lemma BQ_iso1: order_isomorphism (Lf (fun z => z /q (\1q +q z)) BQps BQ_int01) BQps_order BQ_int01_order.
proof: Proof. move: BQps_or_osr BQ_int01_or_osr => [sa sb] [sc sd]. move: eta_likeQps => [[tor _ _ _ _] _]. set f := (fun z => z /q (\1q +q z)). set g := fun z => z /q (\1q -q z). have ha: forall u, inc u BQps -> inc (\1q +q u) BQps. move => u up; exact: (QpsS_sum_rl QpsS1 up). have hb: forall u, inc u BQps -> inc (f u) BQps. move => u up; apply:(QpsS_div up (ha _ up)). have hc: forall u, inc u BQps -> inc (f u) BQ_int01. move => u up; move:(hb _ up) => iup. apply: Zo_i; [ by apply:BQps_sBQ | split; first by apply/ qlt0xP ]. apply /(BQprod_Mlt1 (BQps_sBQ up) (ha _ up)). by rewrite BQsumC;apply:qlt_succ; apply:BQps_sBQ. have hd: bijection (Lf f BQps BQ_int01). apply:lf_bijective. + by move => z zp /=; apply: hc. + move => x y xq yq sf. have aux: forall z, inc z BQps -> z <> \1mq. move => z zp h; rewrite h in zp;exact: (BQ_di_neg_spos QmsSm1 zp). move: (aux _ xq)(aux _ yq) => ax ay. rewrite - (proj1 (BQ_moebius_props1 (BQps_sBQ xq)) ax). rewrite - (proj1 (BQ_moebius_props1 (BQps_sBQ yq)) ay). by rewrite -/(f x) -/(f y) sf. + move => y /Zo_P[yq [/ qlt0xP yp yl1]]; exists (g y); last first. by move: (proj2 (BQ_moebius_props1 yq) (proj2 yl1)). by apply /QpsS_div => //; apply/ qlt0xP; apply/(qlt_diffP1 yq QS1). apply: total_order_isomorphism; aw; trivial. move => x y xp yp /iorder_gleP [/hc fx /hc fy /BQle_P xy]; rewrite !LfV//. apply/iorder_gleP; split => //; apply/BQle_P. move: (BQps_sBQ xp)(BQps_sBQ yp) => xq yq. apply/(BQdiv_Mlelege0 xq (ha _ xp) yq (ha _ yp)). rewrite (BQprodDl yq QS1 xq) (BQprodDr xq QS1 yq). rewrite (BQprod_1l yq) (BQprod_1r xq). by apply /(BQsum_le2r xq yq (QSp xq yq)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)