Lemma istranshzgth ( n m k : hz ) : hzgth n m -> hzgth m k -> hzgth n k . Proof. apply ( istransabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold istrans . apply istransnatgth . Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.