proposition: Lemma BQ_order_isomorphisms_spec2: exists f, order_isomorphism f r' r.
proof: Proof. move: (BQ_order_isomorphisms_spec sqrt2_irrational) => [f fa _]. by exists f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)