proposition: Lemma BR_rational_dichot x: realp x -> rationalp x \/ irrationalp x.
proof: Proof. move => /BR_P rx; case: (p_or_not_p (irrationalp x)); [ by right| by left]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)