proposition: Lemma inv_snum_subproof (xnz : nullity) (xr : reality) (x : {num R & xnz & xr}) : Signed.spec 0 xnz xr (x%:num^-1 : R).
proof: Proof. by case: xr x => [[[]|]|]//= [r]/=; rewrite invr_eq0 ?(invr_ge0, invr_le0) ?realV. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)