proposition: Lemma BQ_iso3 a b: inc a BQps -> ratp b -> order_isomorphism (Lf (fun z => a*q z +q b) BQ BQ) BQ_order BQ_order.
proof: Proof. move => aps bq. move: BQor_sr BQor_tor => pa pb; move: (proj1 pb) => pc. move/ BQps_iP: (aps) => [ap1 anz]; move:(BQp_sBQ ap1) => aq. have pd: lf_axiom (fun z : Set => a *q z +q b) BQ BQ. by move => x xq /=; apply:QSs => //; apply:QSp. apply: total_order_isomorphism; aw; trivial. apply: lf_bijective => //. move => u v uq vq /(BQsum_eq2r (QSp aq uq) (QSp aq vq) bq). by apply/BQprod_eq2l. move => y yq; move:(QS_diff yq bq)=> ybq. exists ((y -q b) /q a); first by apply:QS_div. by rewrite BQprod_div // BQsumC BQsum_diff. move => x y xq yq /BQle_P lexy; rewrite ! LfV//; apply/BQle_P. apply /(BQsum_le2r (QSp aq xq) (QSp aq yq) bq). by rewrite (BQprodC a) (BQprodC a); apply BQprod_Mlege0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)