proposition: Fact pos_divr_closed : divr_closed (@pos R).
proof: Proof. split=> [|x y x_gt0 y_gt0]; rewrite posrE ?ltr01 //. have [Uy|/invr_out->] := boolP (y \is a GRing.unit); last by rewrite pmulr_rgt0. by rewrite -(pmulr_rgt0 _ y_gt0) mulrC divrK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)