proposition: Lemma BRinv_Q x: ratp x -> BRinv (BR_of_Q x) = BR_of_Q (BQinv x).
proof: Proof. by move => xq; rewrite /BRinv (Y_true (BR_of_Q_prop1 xq))(BQ_of_R_prop2 xq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)