proposition: Lemma BQ_iso2: order_isomorphism (Lf (fun z => Yo (z <q \0q) (\1q /q (\1q -q z)) (z +q \1q)) BQ BQps) BQ_order BQps_order.
proof: Proof. move: BQor_sr BQor_tor BQps_or_osr => pa pb [sc sd]. set f :=(fun z => Yo (z <q \0q) (\1q /q (\1q -q z)) (z +q \1q)). have ha: forall x, ratp x -> \1q /q x = BQinv x. move => y yq; rewrite /BQdiv (BQprod_1l (QS_inv yq))//. have hb: lf_axiom f BQ BQps. move =>x xq; rewrite /f; Ytac hc. have qa: inc x BQms by apply/ qgt0xP. have qb :=(QpsS_sum_rl QpsS1 (BQopp_negative1 qa)). apply /(QpsS_div QpsS1 qb). case: (qleT_el QS0 xq) => // / qle0xP hd; exact: (QpsS_sum_r hd QpsS1). have mon: forall x y, x <q y -> f x <q f y. move => x y lexy; move: (lexy) => [[xq yq _] _]. rewrite /f; Ytac hc; Ytac hd. + have qa: inc x BQms by apply/ qgt0xP. have qb :=(QpsS_sum_rl QpsS1 (BQopp_negative1 qa)). have qa': inc y BQms by apply/ qgt0xP. have qb' :=(QpsS_sum_rl QpsS1 (BQopp_negative1 qa')). have qc:= (BQps_sBQ qb'). have qc':= (BQps_sBQ qb). apply /(BQdiv_Mltltge0 QS1 qb QS1 qb'); rewrite BQprod_1l// BQprod_1r //. by apply/(BQsum_lt2l (QSo yq) (QSo xq) QS1) / (qlt_oppP xq yq). + case: (qleT_el QS0 yq) => // / qle0xP yp. move:(BQsum_Mp QS1 yp); rewrite BQsumC; apply:qlt_leT. have qa: inc x BQms by apply/ qgt0xP. have qb:= (BQsum_Mps QS1 (BQopp_negative1 qa)). have qc:= (QpsS_sum_rl QpsS1 (BQopp_negative1 qa)). have qd :=(QpsS_inv qc). move/ BQps_iP: (qc) => [/BQp_sBQ dq dnz]. by move: (BQprod_Mltgt0 qd qb); rewrite BQprod_inv1. + by case hc; BQo_tac. + by apply/(BQsum_lt2r xq yq QS1). apply: total_order_isomorphism; aw; trivial. apply: lf_bijective => //. by move => u v uq vq lxy;case:(qleT_ell uq vq) => // /mon [_] []. move => y yp. move/ BQps_iP: (yp) => [/BQp_sBQ yq ynz]. case: (qleT_el QS1 yq). have hc: y = (y -q \1q) +q \1q by rewrite BQsumC (BQsum_diff QS1 yq). exists (y -q \1q); [ exact (QS_diff yq QS1) | rewrite /f; Ytac h => //]. move /(qgt_diffP yq QS1): h => h1; BQo_tac. move:(proj2 (BQ_moebius_props2 yq) ynz) => hc hd. have he:= (QS_div QS1 yq). have hf:= (QS_diff QS1 he). have hg: \1q -q \1q /q y <q \0q. apply/(qgt_diffP QS1 he). move:(BQprod_Mltgt0 (QpsS_inv yp) hd);rewrite BQprod_inv1 //. by exists (\1q -q \1q /q y) => //; rewrite /f; Ytac0. move => x y xq yq /=; rewrite !LfV//; move/BQle_P => lxy; apply/iorder_gleP. move: (hb _ xq) (hb _ yq) =>sa sb; split => //;apply /BQle_P. case: (equal_or_not x y) => eq;first by rewrite eq; apply: qleR; apply:BQps_sBQ. by move: (mon _ _ (conj lxy eq)) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)