Definition hqlehandmultlinv ( n m k : hq ) ( is : hqgth k 0 ) : hqleh ( k * n ) ( k * m ) -> hqleh n m := negf ( hqgthandmultl _ _ _ is ) .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.