Definition isDivRig_islinv {X : rig} (is : isDivRig X) : ∏ (x : X) (Hx : x != isDivRig_zero is), isDivRig_mult is (isDivRig_inv is (x,, Hx)) x = isDivRig_one is := λ (x : X) (Hx : x != isDivRig_zero is), pr1 (pr2 (pr2 is x Hx)).
Require Import UniMath.MoreFoundations.Tactics.