proposition: Fact real_divr_closed : divr_closed (@real R).
proof: Proof. split=> [|x y Rx Ry]; first by rewrite realE ler01. without loss{Rx} x_ge0: x / 0 <= x. case/orP: Rx => [? | x_le0]; first exact. by rewrite -rpredN -mulNr; apply; rewrite ?oppr_ge0. without loss{Ry} y_ge0: y / 0 <= y; last by rewrite realE -nnegrE rpred_div. case/orP: Ry => [? | y_le0]; first exact. by rewrite -rpredN -mulrN -invrN; apply; rewrite ?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)