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