Lemma hzmultlcan ( a b c : hz ) ( ne : neg ( c = 0 ) ) ( e : ( c * a ) = ( c * b ) ) : a = b .
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.