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