proposition: Lemma invr_gt0 x : (0 < x^-1) = (0 < x).
proof: Proof. have [ux | nux] := boolP (x \is a GRing.unit); last by rewrite invr_out. by apply/idP/idP=> /ltr_pM2r <-; rewrite mul0r (mulrV, mulVr) ?ltr01. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)