proposition: Lemma BR_no_greatest x : ~ (greatest BR_order x).
proof: Proof. move => [xsr xg]. rewrite (proj2 BR_osr) in xsr xg. have [n _ lxn] := (BR_archimedean xsr). move:(xg _ (proj32_1 lxn)) =>/BR_gleP h; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)