Lemma hqgehgthtrans ( n m k : hq ) : hqgeh n m -> hqgth m k -> hqgth n k . Proof. intros gnm gmk . destruct ( hqgehchoice n m gnm ) as [ g' | e ] . apply ( istranshqgth _ _ _ g' gmk ) . rewrite e . apply gmk . Defined.
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.