Definition istranshqleh ( n m k : hq ) : hqleh n m -> hqleh m k -> hqleh n k . Proof. apply istransnegrel . unfold iscotrans. apply iscotranshqgth . Defined.
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.