proposition: Lemma BQ_order_isomorphisms_spec x: irrationalp x -> exists2 f, order_isomorphism f r' r & Vfs f BQps = x.
proof: Proof. move => xi. move: (BQpair_irrational3 xi) => [C [<- [qa qb] qv]]. move /(BQpair_aux2a_equiv2 qa): qb => di. move: qa => [q1 q2 q3 q4 q5]. move: (multiple_interpolation_prop3 (f1 :=fun i => Q (Vg C i)) q5 q4 di qv). by move => [g ga gb]; exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)