proposition: Fact real_addr_closed : addr_closed (@real R).
proof: Proof. split=> [|x y Rx Ry]; first by rewrite realE lexx. without loss{Rx} x_ge0: x y Ry / 0 <= x. case/orP: Rx => [? | x_le0]; first exact. by rewrite -rpredN opprD; apply; rewrite ?rpredN ?oppr_ge0. case/orP: Ry => [y_ge0 | y_le0]; first by rewrite realE -nnegrE rpredD. by rewrite realE -[y]opprK orbC -oppr_ge0 opprB !subr_ge0 ger_leVge ?oppr_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)