proposition: Lemma BRinv_irrational x (aux:= fun z => BQps -s fun_image z BQinv): irrationalp x -> BRinv x = (Yo (inc x BRps) (aux x) (BRopp (aux (BRopp x)))).
proof: Proof. by move => xi; rewrite /BRinv Y_false // => [] [sa sb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)