proposition: Theorem BR_archimedean x: realp x -> exists2 n, natp n & x <r (BR_of_Q (BQ_of_nat n)).
proof: Proof. move => xr. move/BR_P: (xr) => [pa [y yx] pc pd pe]. have yq := (pa _ yx). have ha:= (BR_le_aux2 xr yx). move:(BQ_floorp4 yq) => [n nN le1]. move/(rlt_cQ yq (proj32_1 le1)): le1 => le2. exists n => //; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)