proposition: Lemma BQ_of_R_prop2 x: ratp x -> BQ_of_R (BR_of_Q x) = x.
proof: Proof. move => H; symmetry. have [sa sb]:=(BQ_of_R_prop (BR_of_Q_prop1 H)). by move/(BR_of_Q_inj1 H sb): sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)