proposition: Fact nneg_divr_closed : divr_closed (@nneg R).
proof: Proof. split=> [|x y]; rewrite !nnegrE ?ler01 ?le0r // -!posrE. case/predU1P=> [-> _ | x_gt0]; first by rewrite mul0r eqxx. by case/predU1P=> [-> | y_gt0]; rewrite ?invr0 ?mulr0 ?eqxx // orbC rpred_div. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)