Definition rigneq0andmultrinv (X : rig) (n m : X) (isnm : ((n * m) != 0)%rig) : m != 0%rig. Proof. intros. intro e. rewrite e in isnm. rewrite (rigmultx0 _) in isnm. induction (isnm (idpath _)). Defined.
Require Import UniMath.Algebra.Groups.